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  2287  2eu6  2294  2reu5  3049  ralprg  3758  raltpg  3760  prssg  3849  opelopab2a  4362  opelxp  4801  eqrel  4859  eqrelrel  4870  brcog  4932  dff13  5870  resoprab2  6028  ovig  6056  dfoprab4f  6265  om00el  6661  oeoe  6684  eroveu  6841  th3qlem1  6852  th3qlem2  6853  th3q  6855  ovec  6856  endisj  7037  infxpen  7732  dfac5lem4  7843  sornom  7993  ltsrpr  8789  axcnre  8876  axmulgt0  8987  wloglei  9395  addltmul  10039  ltxr  10549  sumsqeq0  11275  rlim  12065  cpnnen  12604  dvds2lem  12638  gcddvds  12791  opoe  12961  omoe  12962  opeo  12963  omeo  12964  pcqmul  13003  xpsfrnel2  13566  eqgval  14765  frgpuplem  15180  2ndcctbss  17287  txbasval  17407  cnmpt12  17467  cnmpt22  17474  prdsxmslem2  18177  ishtpy  18574  bcthlem1  18850  bcth  18855  volun  19006  vitali  19072  itg1addlem3  19157  rolle  19441  mpfind  19532  mumullem2  20530  lgsquadlem3  20707  lgsquad  20708  2sqlem7  20721  hlimi  21881  leopadd  22826  mulge0b  24492  altopthg  25060  altopthbg  25061  axpasch  25128  brsegle  25290  fzadd2  25768  prtlem13  26059  pellex  26243  dib1dim  31424
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