ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1d Structured version   GIF version

Theorem imbi1d 220
Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbid.1 (φ → (ψχ))
Assertion
Ref Expression
imbi1d (φ → ((ψθ) ↔ (χθ)))

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4 (φ → (ψχ))
21biimprd 147 . . 3 (φ → (χψ))
32imim1d 69 . 2 (φ → ((ψθ) → (χθ)))
41biimpd 132 . . 3 (φ → (ψχ))
54imim1d 69 . 2 (φ → ((χθ) → (ψθ)))
63, 5impbid 120 1 (φ → ((ψθ) ↔ (χθ)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  imbi12d  223  imbi1  225  imim21b  241  pm5.33  529  imordc  784  drsb1  1658  ax11v2  1679  ax11v  1686  ax11ev  1687  equs5or  1689  raleqf  2475  alexeq  2643  mo2icl  2693  sbc19.21g  2799  csbiebg  2862  ralss  2979  ssuni  3572  intmin4  3613  ssexg  3866  pocl  4010  elirr  4204  en2lp  4212  tfisi  4233  vtoclr  4311  sosng  4336  fun11  4888  funimass4  5145  dff13  5328  f1mpt  5331  isopolem  5382  oprabid  5457  caovcan  5584  caoftrn  5655  dfsmo2  5820  qliftfun  6095  ecoptocl  6100  ecopovtrn  6110  ecopovtrng  6113  ltsonq  6251  prarloclem3  6345  lttrsr  6506  axpre-lttrn  6577  bj-rspgt  7224  bdssexg  7319
  Copyright terms: Public domain W3C validator