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

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

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  448  bi2bian9  597  cleqh  2237  abbi  2251  cleqf  2303  vtoclb  2738  vtoclbg  2742  ceqsexg  2808  elabgf  2821  reu6  2868  ru  2903  sbcbig  2950  sbcne12g  3015  sbcnestgf  3046  preq12bg  3695  nalset  4053  undifexmid  4112  exmidsssn  4120  exmidsssnc  4121  exmidundif  4124  opthg  4155  opelopabsb  4177  wetriext  4486  opeliunxp2  4674  resieq  4824  elimasng  4902  cbviota  5088  iota2df  5107  fnbrfvb  5455  fvelimab  5470  fmptco  5579  fsng  5586  fressnfv  5600  funfvima3  5644  isorel  5702  isocnv  5705  isocnv2  5706  isotr  5710  ovg  5902  caovcang  5925  caovordg  5931  caovord3d  5934  caovord  5935  opeliunxp2f  6128  dftpos4  6153  ecopovsym  6518  ecopovsymg  6521  xpf1o  6731  nneneq  6744  supmoti  6873  supsnti  6885  isotilem  6886  isoti  6887  ltanqg  7201  ltmnqg  7202  elinp  7275  prnmaxl  7289  prnminu  7290  ltasrg  7571  axpre-ltadd  7687  zextle  9135  zextlt  9136  xlesubadd  9659  rexfiuz  10754  climshft  11066  dvdsext  11542  ltoddhalfle  11579  halfleoddlt  11580  bezoutlemmo  11683  bezoutlemeu  11684  bezoutlemle  11685  bezoutlemsup  11686  dfgcd3  11687  dvdssq  11708  rpexp  11820  xmeteq0  12517  comet  12657  dedekindeulemuub  12753  dedekindeulemloc  12755  dedekindicclemuub  12762  dedekindicclemloc  12764  bj-nalset  13082  bj-d0clsepcl  13112  bj-nn0sucALT  13165