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  450  bi2bian9  603  cleqh  2270  abbi  2284  cleqf  2337  cbvreuvw  2702  vtoclb  2787  vtoclbg  2791  ceqsexg  2858  elabgf  2872  reu6  2919  ru  2954  sbcbig  3001  sbcne12g  3067  sbcnestgf  3100  preq12bg  3760  nalset  4119  undifexmid  4179  exmidsssn  4188  exmidsssnc  4189  exmidundif  4192  opthg  4223  opelopabsb  4245  wetriext  4561  opeliunxp2  4751  resieq  4901  elimasng  4979  cbviota  5165  iota2df  5184  fnbrfvb  5537  fvelimab  5552  fmptco  5662  fsng  5669  fressnfv  5683  funfvima3  5729  isorel  5787  isocnv  5790  isocnv2  5791  isotr  5795  ovg  5991  caovcang  6014  caovordg  6020  caovord3d  6023  caovord  6024  opeliunxp2f  6217  dftpos4  6242  ecopovsym  6609  ecopovsymg  6612  xpf1o  6822  nneneq  6835  supmoti  6970  supsnti  6982  isotilem  6983  isoti  6984  ltanqg  7362  ltmnqg  7363  elinp  7436  prnmaxl  7450  prnminu  7451  ltasrg  7732  axpre-ltadd  7848  zextle  9303  zextlt  9304  xlesubadd  9840  rexfiuz  10953  climshft  11267  dvdsext  11815  ltoddhalfle  11852  halfleoddlt  11853  bezoutlemmo  11961  bezoutlemeu  11962  bezoutlemle  11963  bezoutlemsup  11964  dfgcd3  11965  dvdssq  11986  rpexp  12107  pcdvdsb  12273  xmeteq0  13153  comet  13293  dedekindeulemuub  13389  dedekindeulemloc  13391  dedekindicclemuub  13398  dedekindicclemloc  13400  logltb  13589  bj-nalset  13930  bj-d0clsepcl  13960  bj-nn0sucALT  14013