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  457  bi2bian9  616  cleqh  2338  abbibcom  2352  abbib  2356  cleqf  2417  cbvreuvw  2792  vtoclb  2880  vtoclbg  2884  ceqsexg  2954  elabgf  2968  reu6  3015  ru  3050  sbcbig  3098  sbcne12g  3165  sbcnestgf  3199  preq12bg  3896  nalset  4261  undifexmid  4328  exmidsssn  4337  exmidsssnc  4338  exmidundif  4341  opthg  4376  opelopabsb  4400  wetriext  4722  opeliunxp2  4918  resieq  5071  elimasng  5153  cbviota  5340  iota2df  5361  fnbrfvb  5738  fvelimab  5756  fmptco  5868  fsng  5875  fressnfv  5896  funfvima3  5946  isorel  6008  isocnv  6011  isocnv2  6012  isotr  6016  ovg  6222  caovcang  6245  caovordg  6251  caovord3d  6254  caovord  6255  uchoice  6365  opeliunxp2f  6503  dftpos4  6528  ecopovsym  6899  ecopovsymg  6902  xpf1o  7138  nneneq  7152  supmoti  7327  supsnti  7339  isotilem  7340  isoti  7341  ltanqg  7761  ltmnqg  7762  elinp  7835  prnmaxl  7849  prnminu  7850  ltasrg  8131  axpre-ltadd  8247  zextle  9720  zextlt  9721  xlesubadd  10268  rexfiuz  11738  climshft  12053  dvdsext  12605  ltoddhalfle  12643  halfleoddlt  12644  bezoutlemmo  12766  bezoutlemeu  12767  bezoutlemle  12768  bezoutlemsup  12769  dfgcd3  12770  dvdssq  12791  rpexp  12914  pcdvdsb  13082  isnsg  13988  nsgbi  13990  elnmz  13994  nmzbi  13995  nmznsg  13999  islidlm  14799  xmeteq0  15443  comet  15583  dedekindeulemuub  15701  dedekindeulemloc  15703  dedekindicclemuub  15710  dedekindicclemloc  15712  logltb  15958  eupth2lem3lem6fi  16695  bj-nalset  16904  bj-d0clsepcl  16934  bj-nn0sucALT  16987  ltlenmkv  17094