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  610  cleqh  2329  abbi  2343  cleqf  2397  cbvreuvw  2771  vtoclb  2858  vtoclbg  2862  ceqsexg  2931  elabgf  2945  reu6  2992  ru  3027  sbcbig  3075  sbcne12g  3142  sbcnestgf  3176  preq12bg  3851  nalset  4214  undifexmid  4277  exmidsssn  4286  exmidsssnc  4287  exmidundif  4290  opthg  4324  opelopabsb  4348  wetriext  4669  opeliunxp2  4862  resieq  5015  elimasng  5096  cbviota  5283  iota2df  5304  fnbrfvb  5674  fvelimab  5692  fmptco  5803  fsng  5810  fressnfv  5830  funfvima3  5877  isorel  5938  isocnv  5941  isocnv2  5942  isotr  5946  ovg  6150  caovcang  6173  caovordg  6179  caovord3d  6182  caovord  6183  uchoice  6289  opeliunxp2f  6390  dftpos4  6415  ecopovsym  6786  ecopovsymg  6789  xpf1o  7013  nneneq  7026  supmoti  7168  supsnti  7180  isotilem  7181  isoti  7182  ltanqg  7595  ltmnqg  7596  elinp  7669  prnmaxl  7683  prnminu  7684  ltasrg  7965  axpre-ltadd  8081  zextle  9546  zextlt  9547  xlesubadd  10087  rexfiuz  11508  climshft  11823  dvdsext  12374  ltoddhalfle  12412  halfleoddlt  12413  bezoutlemmo  12535  bezoutlemeu  12536  bezoutlemle  12537  bezoutlemsup  12538  dfgcd3  12539  dvdssq  12560  rpexp  12683  pcdvdsb  12851  isnsg  13747  nsgbi  13749  elnmz  13753  nmzbi  13754  nmznsg  13758  islidlm  14451  xmeteq0  15041  comet  15181  dedekindeulemuub  15299  dedekindeulemloc  15301  dedekindicclemuub  15308  dedekindicclemloc  15310  logltb  15556  bj-nalset  16282  bj-d0clsepcl  16312  bj-nn0sucALT  16365  ltlenmkv  16468