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

Theorem bibi12d 234
 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 232 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 231 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 187 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm5.32  449  bi2bian9  598  cleqh  2240  abbi  2254  cleqf  2306  vtoclb  2747  vtoclbg  2751  ceqsexg  2818  elabgf  2831  reu6  2878  ru  2913  sbcbig  2960  sbcne12g  3026  sbcnestgf  3057  preq12bg  3709  nalset  4067  undifexmid  4126  exmidsssn  4134  exmidsssnc  4135  exmidundif  4138  opthg  4169  opelopabsb  4191  wetriext  4500  opeliunxp2  4688  resieq  4838  elimasng  4916  cbviota  5102  iota2df  5121  fnbrfvb  5471  fvelimab  5486  fmptco  5595  fsng  5602  fressnfv  5616  funfvima3  5660  isorel  5718  isocnv  5721  isocnv2  5722  isotr  5726  ovg  5918  caovcang  5941  caovordg  5947  caovord3d  5950  caovord  5951  opeliunxp2f  6144  dftpos4  6169  ecopovsym  6534  ecopovsymg  6537  xpf1o  6747  nneneq  6760  supmoti  6890  supsnti  6902  isotilem  6903  isoti  6904  ltanqg  7252  ltmnqg  7253  elinp  7326  prnmaxl  7340  prnminu  7341  ltasrg  7622  axpre-ltadd  7738  zextle  9186  zextlt  9187  xlesubadd  9716  rexfiuz  10813  climshft  11125  dvdsext  11609  ltoddhalfle  11646  halfleoddlt  11647  bezoutlemmo  11750  bezoutlemeu  11751  bezoutlemle  11752  bezoutlemsup  11753  dfgcd3  11754  dvdssq  11775  rpexp  11887  xmeteq0  12587  comet  12727  dedekindeulemuub  12823  dedekindeulemloc  12825  dedekindicclemuub  12832  dedekindicclemloc  12834  logltb  13023  bj-nalset  13284  bj-d0clsepcl  13314  bj-nn0sucALT  13367
 Copyright terms: Public domain W3C validator