Theorem bi2anan9 844

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 686	. 2 |- ( ph -> ( ( ps /\ ta ) <-> ( ch /\ ta ) ) )
3		bi2an9.2	. . 3 |- ( th -> ( ta <-> et ) )
4	3	anbi2d 685	. 2 |- ( th -> ( ( ch /\ ta ) <-> ( ch /\ et ) ) )
5	2, 4	sylan9bb 681	1 |- ( ( ph /\ th ) -> ( ( ps /\ ta ) <-> ( ch /\ et ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359

This theorem is referenced by:  bi2anan9r  845  2mo  2332  2eu6  2339  2reu5  3102  ralprg  3817  raltpg  3819  prssg  3913  prsspwg  3915  opelopab2a  4430  opelxp  4867  eqrel  4924  eqrelrel  4936  brcog  4998  dff13  5963  resoprab2  6126  ovig  6154  dfoprab4f  6364  f1o2ndf1  6413  om00el  6778  oeoe  6801  eroveu  6958  th3qlem1  6969  th3qlem2  6970  th3q  6972  ovec  6973  endisj  7154  infxpen  7852  dfac5lem4  7963  sornom  8113  ltsrpr  8908  axcnre  8995  axmulgt0  9106  wloglei  9515  addltmul  10159  ltxr  10671  sumsqeq0  11415  rlim  12244  cpnnen  12783  dvds2lem  12817  gcddvds  12970  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pcqmul  13182  xpsfrnel2  13745  eqgval  14944  frgpuplem  15359  2ndcctbss  17471  txbasval  17591  cnmpt12  17652  cnmpt22  17659  prdsxmslem2  18512  ishtpy  18950  bcthlem1  19230  bcth  19235  volun  19392  vitali  19458  itg1addlem3  19543  rolle  19827  mpfind  19918  mumullem2  20916  lgsquadlem3  21093  lgsquad  21094  2sqlem7  21107  hlimi  22643  leopadd  23588  isinftm  24204  metidv  24240  mulge0b  25144  altopthg  25716  altopthbg  25717  axpasch  25784  brsegle  25946  itg2addnclem3  26157  fzadd2  26335  prtlem13  26607  pellex  26788  usgra2wlkspthlem1  28036  el2wlkonotot1  28071  frg2wot1  28160  frg2woteqm  28162  dib1dim  31648

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

This theorem depends on definitions:  df-bi 178  df-an 361