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

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
StepHypRef Expression
1 bi2an9.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21anbi1d 686 . 2  |-  ( ph  ->  ( ( ps  /\  ta )  <->  ( ch  /\  ta ) ) )
3 bi2an9.2 . . 3  |-  ( th 
->  ( ta  <->  et )
)
43anbi2d 685 . 2  |-  ( th 
->  ( ( ch  /\  ta )  <->  ( ch  /\  et ) ) )
52, 4sylan9bb 681 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  bi2anan9r  845  2mo  2358  2eu6  2365  2reu5  3134  ralprg  3849  raltpg  3851  prssg  3945  prsspwg  3947  opelopab2a  4462  opelxp  4900  eqrel  4957  eqrelrel  4969  brcog  5031  dff13  5996  resoprab2  6159  ovig  6187  dfoprab4f  6397  f1o2ndf1  6446  om00el  6811  oeoe  6834  eroveu  6991  th3qlem1  7002  th3qlem2  7003  th3q  7005  ovec  7006  endisj  7187  infxpen  7888  dfac5lem4  7999  sornom  8149  ltsrpr  8944  axcnre  9031  axmulgt0  9142  wloglei  9551  addltmul  10195  ltxr  10707  sumsqeq0  11452  rlim  12281  cpnnen  12820  dvds2lem  12854  gcddvds  13007  opoe  13177  omoe  13178  opeo  13179  omeo  13180  pcqmul  13219  xpsfrnel2  13782  eqgval  14981  frgpuplem  15396  2ndcctbss  17510  txbasval  17630  cnmpt12  17691  cnmpt22  17698  prdsxmslem2  18551  ishtpy  18989  bcthlem1  19269  bcth  19274  volun  19431  vitali  19497  itg1addlem3  19582  rolle  19866  mpfind  19957  mumullem2  20955  lgsquadlem3  21132  lgsquad  21133  2sqlem7  21146  hlimi  22682  leopadd  23627  isinftm  24243  metidv  24279  mulge0b  25183  altopthg  25804  altopthbg  25805  axpasch  25872  brsegle  26034  itg2addnclem3  26248  fzadd2  26426  prtlem13  26698  pellex  26879  usgra2wlkspthlem1  28249  el2wlkonotot1  28284  frg2wot1  28373  frg2woteqm  28375  dib1dim  31890
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
  Copyright terms: Public domain W3C validator