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  2moOLDOLD  2369  2eu6OLD  2379  2reu5  3265  ralprg  4023  raltpg  4025  prssg  4126  prsspwg  4128  opelopab2a  4702  opelxp  4967  eqrel  5027  eqrelrel  5039  brcog  5104  dff13  6070  resoprab2  6287  ovig  6312  dfoprab4f  6732  f1o2ndf1  6780  om00el  7115  oeoe  7138  eroveu  7295  th3qlem1  7306  th3qlem2  7307  th3q  7309  ovec  7310  endisj  7498  infxpen  8282  dfac5lem4  8397  sornom  8547  ltsrpr  9345  axcnre  9432  axmulgt0  9550  wloglei  9973  mulge0b  10300  addltmul  10661  ltxr  11196  sumsqeq0  12045  rlim  13075  cpnnen  13613  dvds2lem  13647  gcddvds  13801  opoe  13980  omoe  13981  opeo  13982  omeo  13983  pcqmul  14022  xpsfrnel2  14605  eqgval  15832  frgpuplem  16373  mpfind  17729  2ndcctbss  19175  txbasval  19295  cnmpt12  19356  cnmpt22  19363  prdsxmslem2  20220  ishtpy  20660  bcthlem1  20951  bcth  20956  volun  21142  vitali  21209  itg1addlem3  21292  rolle  21578  mumullem2  22634  lgsquadlem3  22811  lgsquad  22812  2sqlem7  22825  axpasch  23322  hlimi  24725  leopadd  25671  eqrelrd2  26080  isinftm  26332  metidv  26453  altopthg  28132  altopthbg  28133  brsegle  28273  itg2addnclem3  28583  fzadd2  28775  prtlem13  29151  pellex  29314  usgra2wlkspthlem1  30434  el2wlkonotot1  30531  frg2wot1  30788  frg2woteqm  30790  numclwwlkovg  30818  dib1dim  35116