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

Theorem ad2ant2lr 728
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2lr  |-  ( ( ( th  /\  ph )  /\  ( ps  /\  ta ) )  ->  ch )

Proof of Theorem ad2ant2lr
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrr 697 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantll 694 1  |-  ( ( ( th  /\  ph )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  reusv2lem2  4538  mpteqb  5616  omxpenlem  6965  fineqvlem  7079  marypha1lem  7188  fin23lem26  7953  axdc3lem4  8081  mulcmpblnr  8698  ltsrpr  8701  sub4  9094  muladd  9214  ltleadd  9259  divdivdiv  9463  divadddiv  9477  ltmul12a  9614  lt2mul2div  9634  xlemul1a  10610  fzrev  10848  facndiv  11303  fsumconst  12254  isprm5  12793  acsfn2  13567  ghmeql  14707  subgdmdprd  15271  lssvsubcl  15703  lssvacl  15713  lidlsubcl  15970  ocvin  16576  alexsubALTlem2  17744  alexsubALTlem3  17745  blbas  17978  nmoco  18248  cncfmet  18414  cmetcaulem  18716  mbflimsup  19023  ulmdvlem3  19781  ptolemy  19866  grpoideu  20878  ipblnfi  21436  htthlem  21499  hvaddsub4  21659  bralnfn  22530  hmops  22602  hmopm  22603  adjadd  22675  opsqrlem1  22722  atomli  22964  chirredlem2  22973  atcvat3i  22978  mdsymlem5  22989  cdj1i  23015  derangenlem  23704  dfon2lem6  24146  poseq  24255  sltsolem1  24324  prdsbnd  26528  heibor1lem  26544  congneg  27067  jm2.26  27106  lindfmm  27308  hl2at  29667
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