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

Theorem bi2anan9 845
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 687 . 2  |-  ( ph  ->  ( ( ps  /\  ta )  <->  ( ch  /\  ta ) ) )
3 bi2an9.2 . . 3  |-  ( th 
->  ( ta  <->  et )
)
43anbi2d 686 . 2  |-  ( th 
->  ( ( ch  /\  ta )  <->  ( ch  /\  et ) ) )
52, 4sylan9bb 682 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  bi2anan9r  846  2mo  2361  2eu6  2368  2reu5  3144  ralprg  3859  raltpg  3861  prssg  3955  prsspwg  3957  opelopab2a  4473  opelxp  4911  eqrel  4968  eqrelrel  4980  brcog  5042  dff13  6007  resoprab2  6170  ovig  6198  dfoprab4f  6408  f1o2ndf1  6457  om00el  6822  oeoe  6845  eroveu  7002  th3qlem1  7013  th3qlem2  7014  th3q  7016  ovec  7017  endisj  7198  infxpen  7901  dfac5lem4  8012  sornom  8162  ltsrpr  8957  axcnre  9044  axmulgt0  9155  wloglei  9564  addltmul  10208  ltxr  10720  sumsqeq0  11465  rlim  12294  cpnnen  12833  dvds2lem  12867  gcddvds  13020  opoe  13190  omoe  13191  opeo  13192  omeo  13193  pcqmul  13232  xpsfrnel2  13795  eqgval  14994  frgpuplem  15409  2ndcctbss  17523  txbasval  17643  cnmpt12  17704  cnmpt22  17711  prdsxmslem2  18564  ishtpy  19002  bcthlem1  19282  bcth  19287  volun  19444  vitali  19510  itg1addlem3  19593  rolle  19879  mpfind  19970  mumullem2  20968  lgsquadlem3  21145  lgsquad  21146  2sqlem7  21159  hlimi  22695  leopadd  23640  isinftm  24256  metidv  24292  mulge0b  25196  altopthg  25817  altopthbg  25818  axpasch  25885  brsegle  26047  itg2addnclem3  26272  fzadd2  26459  prtlem13  26731  pellex  26912  usgra2wlkspthlem1  28344  el2wlkonotot1  28406  frg2wot1  28520  frg2woteqm  28522  dib1dim  32037
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 179  df-an 362
  Copyright terms: Public domain W3C validator