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  2331  abbi  2345  cleqf  2399  cbvreuvw  2773  vtoclb  2861  vtoclbg  2865  ceqsexg  2934  elabgf  2948  reu6  2995  ru  3030  sbcbig  3078  sbcne12g  3145  sbcnestgf  3179  preq12bg  3856  nalset  4219  undifexmid  4283  exmidsssn  4292  exmidsssnc  4293  exmidundif  4296  opthg  4330  opelopabsb  4354  wetriext  4675  opeliunxp2  4870  resieq  5023  elimasng  5104  cbviota  5291  iota2df  5312  fnbrfvb  5684  fvelimab  5702  fmptco  5813  fsng  5820  fressnfv  5841  funfvima3  5888  isorel  5949  isocnv  5952  isocnv2  5953  isotr  5957  ovg  6161  caovcang  6184  caovordg  6190  caovord3d  6193  caovord  6194  uchoice  6300  opeliunxp2f  6404  dftpos4  6429  ecopovsym  6800  ecopovsymg  6803  xpf1o  7030  nneneq  7043  supmoti  7192  supsnti  7204  isotilem  7205  isoti  7206  ltanqg  7620  ltmnqg  7621  elinp  7694  prnmaxl  7708  prnminu  7709  ltasrg  7990  axpre-ltadd  8106  zextle  9571  zextlt  9572  xlesubadd  10118  rexfiuz  11551  climshft  11866  dvdsext  12418  ltoddhalfle  12456  halfleoddlt  12457  bezoutlemmo  12579  bezoutlemeu  12580  bezoutlemle  12581  bezoutlemsup  12582  dfgcd3  12583  dvdssq  12604  rpexp  12727  pcdvdsb  12895  isnsg  13791  nsgbi  13793  elnmz  13797  nmzbi  13798  nmznsg  13802  islidlm  14496  xmeteq0  15086  comet  15226  dedekindeulemuub  15344  dedekindeulemloc  15346  dedekindicclemuub  15353  dedekindicclemloc  15355  logltb  15601  eupth2lem3lem6fi  16325  bj-nalset  16511  bj-d0clsepcl  16541  bj-nn0sucALT  16594  ltlenmkv  16695