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  2296  abbi  2310  cleqf  2364  cbvreuvw  2735  vtoclb  2821  vtoclbg  2825  ceqsexg  2892  elabgf  2906  reu6  2953  ru  2988  sbcbig  3036  sbcne12g  3102  sbcnestgf  3136  preq12bg  3804  nalset  4164  undifexmid  4227  exmidsssn  4236  exmidsssnc  4237  exmidundif  4240  opthg  4272  opelopabsb  4295  wetriext  4614  opeliunxp2  4807  resieq  4957  elimasng  5038  cbviota  5225  iota2df  5245  fnbrfvb  5604  fvelimab  5620  fmptco  5731  fsng  5738  fressnfv  5752  funfvima3  5799  isorel  5858  isocnv  5861  isocnv2  5862  isotr  5866  ovg  6066  caovcang  6089  caovordg  6095  caovord3d  6098  caovord  6099  uchoice  6204  opeliunxp2f  6305  dftpos4  6330  ecopovsym  6699  ecopovsymg  6702  xpf1o  6914  nneneq  6927  supmoti  7068  supsnti  7080  isotilem  7081  isoti  7082  ltanqg  7484  ltmnqg  7485  elinp  7558  prnmaxl  7572  prnminu  7573  ltasrg  7854  axpre-ltadd  7970  zextle  9434  zextlt  9435  xlesubadd  9975  rexfiuz  11171  climshft  11486  dvdsext  12037  ltoddhalfle  12075  halfleoddlt  12076  bezoutlemmo  12198  bezoutlemeu  12199  bezoutlemle  12200  bezoutlemsup  12201  dfgcd3  12202  dvdssq  12223  rpexp  12346  pcdvdsb  12514  isnsg  13408  nsgbi  13410  elnmz  13414  nmzbi  13415  nmznsg  13419  islidlm  14111  xmeteq0  14679  comet  14819  dedekindeulemuub  14937  dedekindeulemloc  14939  dedekindicclemuub  14946  dedekindicclemloc  14948  logltb  15194  bj-nalset  15625  bj-d0clsepcl  15655  bj-nn0sucALT  15708  ltlenmkv  15801