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  4265  undifexmid  4332  exmidsssn  4341  exmidsssnc  4342  exmidundif  4345  opthg  4380  opelopabsb  4404  wetriext  4726  opeliunxp2  4922  resieq  5075  elimasng  5158  cbviota  5345  iota2df  5366  fnbrfvb  5744  fvelimab  5762  fmptco  5877  fsng  5884  fressnfv  5905  funfvima3  5955  isorel  6017  isocnv  6020  isocnv2  6021  isotr  6025  ovg  6231  caovcang  6254  caovordg  6260  caovord3d  6263  caovord  6264  uchoice  6375  opeliunxp2f  6513  dftpos4  6538  ecopovsym  6909  ecopovsymg  6912  xpf1o  7149  nneneq  7163  supmoti  7340  supsnti  7352  isotilem  7353  isoti  7354  ltanqg  7774  ltmnqg  7775  elinp  7848  prnmaxl  7862  prnminu  7863  ltasrg  8144  axpre-ltadd  8260  zextle  9749  zextlt  9750  xlesubadd  10303  rexfiuz  11778  climshft  12096  dvdsext  12648  ltoddhalfle  12686  halfleoddlt  12687  bezoutlemmo  12809  bezoutlemeu  12810  bezoutlemle  12811  bezoutlemsup  12812  dfgcd3  12813  dvdssq  12834  rpexp  12958  pcdvdsb  13129  isnsg  14065  nsgbi  14067  elnmz  14071  nmzbi  14072  nmznsg  14076  gsumcom2fi  14276  islidlm  14926  xmeteq0  15597  comet  15737  dedekindeulemuub  15855  dedekindeulemloc  15857  dedekindicclemuub  15864  dedekindicclemloc  15866  logltb  16116  eupth2lem3lem6fi  16929  bj-nalset  17138  bj-d0clsepcl  17168  bj-nn0sucALT  17221  ltlenmkv  17339