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 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32  453  bi2bian9  612  cleqh  2332  abbibcom  2346  abbib  2350  cleqf  2409  cbvreuvw  2783  vtoclb  2871  vtoclbg  2875  ceqsexg  2944  elabgf  2958  reu6  3005  ru  3040  sbcbig  3088  sbcne12g  3155  sbcnestgf  3189  preq12bg  3876  nalset  4239  undifexmid  4305  exmidsssn  4314  exmidsssnc  4315  exmidundif  4318  opthg  4353  opelopabsb  4377  wetriext  4698  opeliunxp2  4894  resieq  5047  elimasng  5129  cbviota  5316  iota2df  5337  fnbrfvb  5714  fvelimab  5732  fmptco  5842  fsng  5849  fressnfv  5870  funfvima3  5919  isorel  5980  isocnv  5983  isocnv2  5984  isotr  5988  ovg  6192  caovcang  6215  caovordg  6221  caovord3d  6224  caovord  6225  uchoice  6330  opeliunxp2f  6468  dftpos4  6493  ecopovsym  6864  ecopovsymg  6867  xpf1o  7096  nneneq  7110  supmoti  7283  supsnti  7295  isotilem  7296  isoti  7297  ltanqg  7711  ltmnqg  7712  elinp  7785  prnmaxl  7799  prnminu  7800  ltasrg  8081  axpre-ltadd  8197  zextle  9665  zextlt  9666  xlesubadd  10212  rexfiuz  11667  climshft  11982  dvdsext  12534  ltoddhalfle  12572  halfleoddlt  12573  bezoutlemmo  12695  bezoutlemeu  12696  bezoutlemle  12697  bezoutlemsup  12698  dfgcd3  12699  dvdssq  12720  rpexp  12843  pcdvdsb  13011  isnsg  13908  nsgbi  13910  elnmz  13914  nmzbi  13915  nmznsg  13919  islidlm  14614  xmeteq0  15211  comet  15351  dedekindeulemuub  15469  dedekindeulemloc  15471  dedekindicclemuub  15478  dedekindicclemloc  15480  logltb  15726  eupth2lem3lem6fi  16453  bj-nalset  16652  bj-d0clsepcl  16682  bj-nn0sucALT  16735  ltlenmkv  16842