Theorem bi2anan9 868

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)

Hypotheses

Ref	Expression
bi2an9.1	|- ( ph -> ( ps <-> ch ) )
bi2an9.2	|- ( th -> ( ta <-> et ) )

Assertion

Ref	Expression
bi2anan9	|- ( ( ph /\ th ) -> ( ( ps /\ ta ) <-> ( ch /\ et ) ) )

Proof of Theorem bi2anan9

Step	Hyp	Ref	Expression
1		bi2an9.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	anbi1d 704	. 2 |- ( ph -> ( ( ps /\ ta ) <-> ( ch /\ ta ) ) )
3		bi2an9.2	. . 3 |- ( th -> ( ta <-> et ) )
4	3	anbi2d 703	. 2 |- ( th -> ( ( ch /\ ta ) <-> ( ch /\ et ) ) )
5	2, 4	sylan9bb 699	1 |- ( ( ph /\ th ) -> ( ( ps /\ ta ) <-> ( ch /\ et ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  bi2anan9r  869  2mo  2357  2moOLD  2358  2moOLDOLD  2359  2eu6OLD  2368  2reu5  3162  ralprg  3920  raltpg  3922  prssg  4023  prsspwg  4025  opelopab2a  4599  opelxp  4864  eqrel  4924  eqrelrel  4936  brcog  5001  dff13  5966  resoprab2  6182  ovig  6207  dfoprab4f  6627  f1o2ndf1  6675  om00el  7007  oeoe  7030  eroveu  7187  th3qlem1  7198  th3qlem2  7199  th3q  7201  ovec  7202  endisj  7390  infxpen  8173  dfac5lem4  8288  sornom  8438  ltsrpr  9236  axcnre  9323  axmulgt0  9441  wloglei  9864  mulge0b  10191  addltmul  10552  ltxr  11087  sumsqeq0  11936  rlim  12965  cpnnen  13503  dvds2lem  13537  gcddvds  13691  opoe  13870  omoe  13871  opeo  13872  omeo  13873  pcqmul  13912  xpsfrnel2  14495  eqgval  15721  frgpuplem  16260  mpfind  17602  2ndcctbss  19039  txbasval  19159  cnmpt12  19220  cnmpt22  19227  prdsxmslem2  20084  ishtpy  20524  bcthlem1  20815  bcth  20820  volun  21006  vitali  21073  itg1addlem3  21156  rolle  21442  mumullem2  22498  lgsquadlem3  22675  lgsquad  22676  2sqlem7  22689  axpasch  23155  hlimi  24558  leopadd  25504  eqrelrd2  25914  isinftm  26166  metidv  26288  altopthg  27967  altopthbg  27968  brsegle  28108  itg2addnclem3  28416  fzadd2  28608  prtlem13  28984  pellex  29147  usgra2wlkspthlem1  30267  el2wlkonotot1  30364  frg2wot1  30621  frg2woteqm  30623  numclwwlkovg  30651  dib1dim  34703