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  608  cleqh  2306  abbi  2320  cleqf  2374  cbvreuvw  2745  vtoclb  2832  vtoclbg  2836  ceqsexg  2905  elabgf  2919  reu6  2966  ru  3001  sbcbig  3049  sbcne12g  3115  sbcnestgf  3149  preq12bg  3820  nalset  4182  undifexmid  4245  exmidsssn  4254  exmidsssnc  4255  exmidundif  4258  opthg  4290  opelopabsb  4314  wetriext  4633  opeliunxp2  4826  resieq  4978  elimasng  5059  cbviota  5246  iota2df  5266  fnbrfvb  5632  fvelimab  5648  fmptco  5759  fsng  5766  fressnfv  5784  funfvima3  5831  isorel  5890  isocnv  5893  isocnv2  5894  isotr  5898  ovg  6098  caovcang  6121  caovordg  6127  caovord3d  6130  caovord  6131  uchoice  6236  opeliunxp2f  6337  dftpos4  6362  ecopovsym  6731  ecopovsymg  6734  xpf1o  6956  nneneq  6969  supmoti  7110  supsnti  7122  isotilem  7123  isoti  7124  ltanqg  7533  ltmnqg  7534  elinp  7607  prnmaxl  7621  prnminu  7622  ltasrg  7903  axpre-ltadd  8019  zextle  9484  zextlt  9485  xlesubadd  10025  rexfiuz  11375  climshft  11690  dvdsext  12241  ltoddhalfle  12279  halfleoddlt  12280  bezoutlemmo  12402  bezoutlemeu  12403  bezoutlemle  12404  bezoutlemsup  12405  dfgcd3  12406  dvdssq  12427  rpexp  12550  pcdvdsb  12718  isnsg  13613  nsgbi  13615  elnmz  13619  nmzbi  13620  nmznsg  13624  islidlm  14316  xmeteq0  14906  comet  15046  dedekindeulemuub  15164  dedekindeulemloc  15166  dedekindicclemuub  15173  dedekindicclemloc  15175  logltb  15421  bj-nalset  15969  bj-d0clsepcl  15999  bj-nn0sucALT  16052  ltlenmkv  16150