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  4536  mpteqb  5614  omxpenlem  6963  fineqvlem  7077  marypha1lem  7186  fin23lem26  7951  axdc3lem4  8079  mulcmpblnr  8696  ltsrpr  8699  sub4  9092  muladd  9212  ltleadd  9257  divdivdiv  9461  divadddiv  9475  ltmul12a  9612  lt2mul2div  9632  xlemul1a  10608  fzrev  10846  facndiv  11301  fsumconst  12252  isprm5  12791  acsfn2  13565  ghmeql  14705  subgdmdprd  15269  lssvsubcl  15701  lssvacl  15711  lidlsubcl  15968  ocvin  16574  alexsubALTlem2  17742  alexsubALTlem3  17743  blbas  17976  nmoco  18246  cncfmet  18412  cmetcaulem  18714  mbflimsup  19021  ulmdvlem3  19779  ptolemy  19864  grpoideu  20876  ipblnfi  21434  htthlem  21497  hvaddsub4  21657  bralnfn  22528  hmops  22600  hmopm  22601  adjadd  22673  opsqrlem1  22720  atomli  22962  chirredlem2  22971  atcvat3i  22976  mdsymlem5  22987  cdj1i  23013  derangenlem  23702  dfon2lem6  24144  poseq  24253  sltsolem1  24322  prdsbnd  26517  heibor1lem  26533  congneg  27056  jm2.26  27095  lindfmm  27297  hl2at  29594
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