ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1d 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  541  imordc  796  drsb1  1680  ax11v2  1701  ax11v  1708  ax11ev  1709  equs5or  1711  raleqf  2498  alexeq  2667  mo2icl  2717  sbc19.21g  2823  csbiebg  2886  ralss  3003  ssuni  3596  intmin4  3637  ssexg  3890  pocl  4034  elirr  4227  en2lp  4235  tfisi  4256  vtoclr  4334  sosng  4359  fun11  4912  funimass4  5170  dff13  5353  f1mpt  5356  isopolem  5407  oprabid  5483  caovcan  5610  caoftrn  5681  dfsmo2  5847  qliftfun  6128  ecoptocl  6133  ecopovtrn  6143  ecopovtrng  6146  dom2lem  6192  ssfiexmid  6258  ltsonq  6386  prarloclem3  6485  lttrsr  6737  mulextsr1  6755  axpre-lttrn  6848  axpre-mulext  6852  axcaucvglemres  6863  prime  8205  raluz  8389  indstr  8404  fz1sbc  8820  caucvgre  9300  bj-rspgt  9368  bdssexg  9467
  Copyright terms: Public domain W3C validator