Theorem bibi12d 234

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 232	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 231	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 187	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.32  446  bi2bian9  580  cleqh  2214  abbi  2228  cleqf  2279  vtoclb  2714  vtoclbg  2718  ceqsexg  2783  elabgf  2796  reu6  2842  ru  2877  sbcbig  2923  sbcne12g  2987  sbcnestgf  3017  preq12bg  3666  nalset  4018  undifexmid  4077  exmidsssn  4085  exmidsssnc  4086  exmidundif  4089  opthg  4120  opelopabsb  4142  wetriext  4451  opeliunxp2  4639  resieq  4787  elimasng  4865  cbviota  5051  iota2df  5070  fnbrfvb  5416  fvelimab  5431  fmptco  5540  fsng  5547  fressnfv  5561  funfvima3  5605  isorel  5663  isocnv  5666  isocnv2  5667  isotr  5671  ovg  5863  caovcang  5886  caovordg  5892  caovord3d  5895  caovord  5896  opeliunxp2f  6089  dftpos4  6114  ecopovsym  6479  ecopovsymg  6482  xpf1o  6691  nneneq  6704  supmoti  6832  supsnti  6844  isotilem  6845  isoti  6846  ltanqg  7156  ltmnqg  7157  elinp  7230  prnmaxl  7244  prnminu  7245  ltasrg  7513  axpre-ltadd  7621  zextle  9046  zextlt  9047  xlesubadd  9559  rexfiuz  10653  climshft  10965  dvdsext  11401  ltoddhalfle  11438  halfleoddlt  11439  bezoutlemmo  11540  bezoutlemeu  11541  bezoutlemle  11542  bezoutlemsup  11543  dfgcd3  11544  dvdssq  11565  rpexp  11677  xmeteq0  12348  comet  12488  bj-nalset  12785  bj-d0clsepcl  12815  bj-nn0sucALT  12868