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

Theorem bibi12d 224
 Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1 (𝜑 → (𝜓𝜒))
imbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
bibi12d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))

Proof of Theorem bibi12d
StepHypRef Expression
1 imbi12d.1 . . 3 (𝜑 → (𝜓𝜒))
21bibi1d 222 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 221 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 177 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:  pm5.32  426  bi2bian9  540  cleqh  2137  abbi  2151  cleqf  2201  vtoclb  2611  vtoclbg  2614  ceqsexg  2672  elabgf  2685  reu6  2730  ru  2763  sbcbig  2809  sbcne12g  2868  sbcnestgf  2897  preq12bg  3544  nalset  3887  opthg  3975  opelopabsb  3997  wetriext  4301  opeliunxp2  4476  resieq  4622  elimasng  4693  cbviota  4872  iota2df  4891  fnbrfvb  5214  fvelimab  5229  fmptco  5330  fsng  5336  fressnfv  5350  funfvima3  5392  isorel  5448  isocnv  5451  isocnv2  5452  isotr  5456  ovg  5639  caovcang  5662  caovordg  5668  caovord3d  5671  caovord  5672  dftpos4  5878  ecopovsym  6202  ecopovsymg  6205  nneneq  6320  ltanqg  6498  ltmnqg  6499  elinp  6572  prnmaxl  6586  prnminu  6587  ltasrg  6855  axpre-ltadd  6960  zextle  8331  zextlt  8332  climshft  9825  bj-nalset  10015  bj-d0clsepcl  10049  bj-nn0sucALT  10103
 Copyright terms: Public domain W3C validator