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  7486  ltmnqg  7487  elinp  7560  prnmaxl  7574  prnminu  7575  ltasrg  7856  axpre-ltadd  7972  zextle  9436  zextlt  9437  xlesubadd  9977  rexfiuz  11173  climshft  11488  dvdsext  12039  ltoddhalfle  12077  halfleoddlt  12078  bezoutlemmo  12200  bezoutlemeu  12201  bezoutlemle  12202  bezoutlemsup  12203  dfgcd3  12204  dvdssq  12225  rpexp  12348  pcdvdsb  12516  isnsg  13410  nsgbi  13412  elnmz  13416  nmzbi  13417  nmznsg  13421  islidlm  14113  xmeteq0  14703  comet  14843  dedekindeulemuub  14961  dedekindeulemloc  14963  dedekindicclemuub  14970  dedekindicclemloc  14972  logltb  15218  bj-nalset  15649  bj-d0clsepcl  15679  bj-nn0sucALT  15732  ltlenmkv  15827