Theorem bi2anan9 869

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  870  2moOLDOLD  2377  2eu6OLD  2387  2reu5  3305  ralprg  4069  raltpg  4071  prssg  4175  prsspwg  4177  opelopab2a  4755  opelxp  5021  eqrel  5083  eqrelrel  5095  brcog  5160  dff13  6145  resoprab2  6374  ovig  6399  dfoprab4f  6832  f1o2ndf1  6881  om00el  7215  oeoe  7238  eroveu  7396  endisj  7594  infxpen  8381  dfac5lem4  8496  sornom  8646  ltsrpr  9443  axcnre  9530  axmulgt0  9648  wloglei  10074  mulge0b  10401  addltmul  10763  ltxr  11313  sumsqeq0  12201  rlim  13267  cpnnen  13812  dvds2lem  13846  gcddvds  14001  opoe  14183  omoe  14184  opeo  14185  omeo  14186  pcqmul  14225  xpsfrnel2  14809  eqgval  16038  frgpuplem  16579  mpfind  17969  2ndcctbss  19715  txbasval  19835  cnmpt12  19896  cnmpt22  19903  prdsxmslem2  20760  ishtpy  21200  bcthlem1  21491  bcth  21496  volun  21683  vitali  21750  itg1addlem3  21833  rolle  22119  mumullem2  23175  lgsquadlem3  23352  lgsquad  23353  2sqlem7  23366  axpasch  23913  usgra2adedgwlkonALT  24278  usgra2wlkspthlem1  24281  el2wlkonotot1  24536  hlimi  25631  leopadd  26577  eqrelrd2  26990  isinftm  27237  metidv  27357  altopthg  29044  altopthbg  29045  brsegle  29185  itg2addnclem3  29496  fzadd2  29688  prtlem13  30064  pellex  30226  frg2wot1  31776  frg2woteqm  31778  numclwwlkovg  31806  dib1dim  35837