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  2948  elabgf  2962  reu6  3009  ru  3044  sbcbig  3092  sbcne12g  3159  sbcnestgf  3193  preq12bg  3882  nalset  4245  undifexmid  4311  exmidsssn  4320  exmidsssnc  4321  exmidundif  4324  opthg  4359  opelopabsb  4383  wetriext  4704  opeliunxp2  4900  resieq  5053  elimasng  5135  cbviota  5322  iota2df  5343  fnbrfvb  5720  fvelimab  5738  fmptco  5848  fsng  5855  fressnfv  5876  funfvima3  5925  isorel  5987  isocnv  5990  isocnv2  5991  isotr  5995  ovg  6201  caovcang  6224  caovordg  6230  caovord3d  6233  caovord  6234  uchoice  6344  opeliunxp2f  6482  dftpos4  6507  ecopovsym  6878  ecopovsymg  6881  xpf1o  7110  nneneq  7124  supmoti  7297  supsnti  7309  isotilem  7310  isoti  7311  ltanqg  7731  ltmnqg  7732  elinp  7805  prnmaxl  7819  prnminu  7820  ltasrg  8101  axpre-ltadd  8217  zextle  9690  zextlt  9691  xlesubadd  10238  rexfiuz  11702  climshft  12017  dvdsext  12569  ltoddhalfle  12607  halfleoddlt  12608  bezoutlemmo  12730  bezoutlemeu  12731  bezoutlemle  12732  bezoutlemsup  12733  dfgcd3  12734  dvdssq  12755  rpexp  12878  pcdvdsb  13046  isnsg  13958  nsgbi  13960  elnmz  13964  nmzbi  13965  nmznsg  13969  islidlm  14756  xmeteq0  15353  comet  15493  dedekindeulemuub  15611  dedekindeulemloc  15613  dedekindicclemuub  15620  dedekindicclemloc  15622  logltb  15868  eupth2lem3lem6fi  16595  bj-nalset  16804  bj-d0clsepcl  16834  bj-nn0sucALT  16887  ltlenmkv  16995