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  2334  abbibcom  2348  abbib  2352  cleqf  2411  cbvreuvw  2786  vtoclb  2874  vtoclbg  2878  ceqsexg  2947  elabgf  2961  reu6  3008  ru  3043  sbcbig  3091  sbcne12g  3158  sbcnestgf  3192  preq12bg  3879  nalset  4242  undifexmid  4308  exmidsssn  4317  exmidsssnc  4318  exmidundif  4321  opthg  4356  opelopabsb  4380  wetriext  4701  opeliunxp2  4897  resieq  5050  elimasng  5132  cbviota  5319  iota2df  5340  fnbrfvb  5717  fvelimab  5735  fmptco  5845  fsng  5852  fressnfv  5873  funfvima3  5922  isorel  5983  isocnv  5986  isocnv2  5987  isotr  5991  ovg  6195  caovcang  6218  caovordg  6224  caovord3d  6227  caovord  6228  uchoice  6333  opeliunxp2f  6471  dftpos4  6496  ecopovsym  6867  ecopovsymg  6870  xpf1o  7099  nneneq  7113  supmoti  7286  supsnti  7298  isotilem  7299  isoti  7300  ltanqg  7720  ltmnqg  7721  elinp  7794  prnmaxl  7808  prnminu  7809  ltasrg  8090  axpre-ltadd  8206  zextle  9675  zextlt  9676  xlesubadd  10222  rexfiuz  11682  climshft  11997  dvdsext  12549  ltoddhalfle  12587  halfleoddlt  12588  bezoutlemmo  12710  bezoutlemeu  12711  bezoutlemle  12712  bezoutlemsup  12713  dfgcd3  12714  dvdssq  12735  rpexp  12858  pcdvdsb  13026  isnsg  13940  nsgbi  13942  elnmz  13946  nmzbi  13947  nmznsg  13951  islidlm  14676  xmeteq0  15273  comet  15413  dedekindeulemuub  15531  dedekindeulemloc  15533  dedekindicclemuub  15540  dedekindicclemloc  15542  logltb  15788  eupth2lem3lem6fi  16515  bj-nalset  16714  bj-d0clsepcl  16744  bj-nn0sucALT  16797  ltlenmkv  16905