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-mp 5  ax-1 6  ax-2 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  449  bi2bian9  598  cleqh  2266  abbi  2280  cleqf  2333  cbvreuvw  2698  vtoclb  2783  vtoclbg  2787  ceqsexg  2854  elabgf  2868  reu6  2915  ru  2950  sbcbig  2997  sbcne12g  3063  sbcnestgf  3096  preq12bg  3753  nalset  4112  undifexmid  4172  exmidsssn  4181  exmidsssnc  4182  exmidundif  4185  opthg  4216  opelopabsb  4238  wetriext  4554  opeliunxp2  4744  resieq  4894  elimasng  4972  cbviota  5158  iota2df  5177  fnbrfvb  5527  fvelimab  5542  fmptco  5651  fsng  5658  fressnfv  5672  funfvima3  5718  isorel  5776  isocnv  5779  isocnv2  5780  isotr  5784  ovg  5980  caovcang  6003  caovordg  6009  caovord3d  6012  caovord  6013  opeliunxp2f  6206  dftpos4  6231  ecopovsym  6597  ecopovsymg  6600  xpf1o  6810  nneneq  6823  supmoti  6958  supsnti  6970  isotilem  6971  isoti  6972  ltanqg  7341  ltmnqg  7342  elinp  7415  prnmaxl  7429  prnminu  7430  ltasrg  7711  axpre-ltadd  7827  zextle  9282  zextlt  9283  xlesubadd  9819  rexfiuz  10931  climshft  11245  dvdsext  11793  ltoddhalfle  11830  halfleoddlt  11831  bezoutlemmo  11939  bezoutlemeu  11940  bezoutlemle  11941  bezoutlemsup  11942  dfgcd3  11943  dvdssq  11964  rpexp  12085  pcdvdsb  12251  xmeteq0  12999  comet  13139  dedekindeulemuub  13235  dedekindeulemloc  13237  dedekindicclemuub  13244  dedekindicclemloc  13246  logltb  13435  bj-nalset  13777  bj-d0clsepcl  13807  bj-nn0sucALT  13860