MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bi2anan9 Unicode version

Theorem bi2anan9 843
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
StepHypRef Expression
1 bi2an9.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21anbi1d 685 . 2  |-  ( ph  ->  ( ( ps  /\  ta )  <->  ( ch  /\  ta ) ) )
3 bi2an9.2 . . 3  |-  ( th 
->  ( ta  <->  et )
)
43anbi2d 684 . 2  |-  ( th 
->  ( ( ch  /\  ta )  <->  ( ch  /\  et ) ) )
52, 4sylan9bb 680 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  bi2anan9r  844  2mo  2221  2eu6  2228  2reu5  2973  ralprg  3682  raltpg  3684  prssg  3770  opelopab2a  4280  opelxp  4719  eqrel  4777  eqrelrel  4788  brcog  4850  dff13  5783  resoprab2  5941  ovig  5969  dfoprab4f  6178  om00el  6574  oeoe  6597  eroveu  6753  th3qlem1  6764  th3qlem2  6765  th3q  6767  ovec  6768  endisj  6949  infxpen  7642  dfac5lem4  7753  sornom  7903  ltsrpr  8699  axcnre  8786  axmulgt0  8897  wloglei  9305  addltmul  9947  ltxr  10457  sumsqeq0  11182  rlim  11969  cpnnen  12507  dvds2lem  12541  gcddvds  12694  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pcqmul  12906  xpsfrnel2  13467  eqgval  14666  frgpuplem  15081  2ndcctbss  17181  txbasval  17301  cnmpt12  17361  cnmpt22  17368  prdsxmslem2  18075  ishtpy  18470  bcthlem1  18746  bcth  18751  volun  18902  vitali  18968  itg1addlem3  19053  rolle  19337  mpfind  19428  mumullem2  20418  lgsquadlem3  20595  lgsquad  20596  2sqlem7  20609  hlimi  21767  leopadd  22712  mulge0b  24086  altopthg  24501  altopthbg  24502  axpasch  24569  brsegle  24731  int2pre  25237  ishomb  25788  fzadd2  26444  prtlem13  26736  pellex  26920  dib1dim  31355
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 177  df-an 360
  Copyright terms: Public domain W3C validator