MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bi2anan9 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  2340  2eu6  2347  2reu5  3110  ralprg  3825  raltpg  3827  prssg  3921  prsspwg  3923  opelopab2a  4438  opelxp  4875  eqrel  4932  eqrelrel  4944  brcog  5006  dff13  5971  resoprab2  6134  ovig  6162  dfoprab4f  6372  f1o2ndf1  6421  om00el  6786  oeoe  6809  eroveu  6966  th3qlem1  6977  th3qlem2  6978  th3q  6980  ovec  6981  endisj  7162  infxpen  7860  dfac5lem4  7971  sornom  8121  ltsrpr  8916  axcnre  9003  axmulgt0  9114  wloglei  9523  addltmul  10167  ltxr  10679  sumsqeq0  11423  rlim  12252  cpnnen  12791  dvds2lem  12825  gcddvds  12978  opoe  13148  omoe  13149  opeo  13150  omeo  13151  pcqmul  13190  xpsfrnel2  13753  eqgval  14952  frgpuplem  15367  2ndcctbss  17479  txbasval  17599  cnmpt12  17660  cnmpt22  17667  prdsxmslem2  18520  ishtpy  18958  bcthlem1  19238  bcth  19243  volun  19400  vitali  19466  itg1addlem3  19551  rolle  19835  mpfind  19926  mumullem2  20924  lgsquadlem3  21101  lgsquad  21102  2sqlem7  21115  hlimi  22651  leopadd  23596  isinftm  24212  metidv  24248  mulge0b  25152  altopthg  25724  altopthbg  25725  axpasch  25792  brsegle  25954  itg2addnclem3  26165  fzadd2  26343  prtlem13  26615  pellex  26796  usgra2wlkspthlem1  28044  el2wlkonotot1  28079  frg2wot1  28168  frg2woteqm  28170  dib1dim  31660
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