Theorem bibi12d 235

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

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	bibi1d 233	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 232	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.32  457  bi2bian9  616  cleqh  2338  abbibcom  2352  abbib  2356  cleqf  2417  cbvreuvw  2792  vtoclb  2880  vtoclbg  2884  ceqsexg  2954  elabgf  2968  reu6  3015  ru  3050  sbcbig  3098  sbcne12g  3165  sbcnestgf  3199  preq12bg  3898  nalset  4263  undifexmid  4330  exmidsssn  4339  exmidsssnc  4340  exmidundif  4343  opthg  4378  opelopabsb  4402  wetriext  4724  opeliunxp2  4920  resieq  5073  elimasng  5155  cbviota  5342  iota2df  5363  fnbrfvb  5741  fvelimab  5759  fmptco  5874  fsng  5881  fressnfv  5902  funfvima3  5952  isorel  6014  isocnv  6017  isocnv2  6018  isotr  6022  ovg  6228  caovcang  6251  caovordg  6257  caovord3d  6260  caovord  6261  uchoice  6371  opeliunxp2f  6509  dftpos4  6534  ecopovsym  6905  ecopovsymg  6908  xpf1o  7144  nneneq  7158  supmoti  7333  supsnti  7345  isotilem  7346  isoti  7347  ltanqg  7767  ltmnqg  7768  elinp  7841  prnmaxl  7855  prnminu  7856  ltasrg  8137  axpre-ltadd  8253  zextle  9739  zextlt  9740  xlesubadd  10287  rexfiuz  11757  climshft  12072  dvdsext  12624  ltoddhalfle  12662  halfleoddlt  12663  bezoutlemmo  12785  bezoutlemeu  12786  bezoutlemle  12787  bezoutlemsup  12788  dfgcd3  12789  dvdssq  12810  rpexp  12933  pcdvdsb  13101  isnsg  14007  nsgbi  14009  elnmz  14013  nmzbi  14014  nmznsg  14018  islidlm  14818  xmeteq0  15462  comet  15602  dedekindeulemuub  15720  dedekindeulemloc  15722  dedekindicclemuub  15729  dedekindicclemloc  15731  logltb  15979  eupth2lem3lem6fi  16724  bj-nalset  16933  bj-d0clsepcl  16963  bj-nn0sucALT  17016  ltlenmkv  17132