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  4552  mpteqb  5630  omxpenlem  6979  fineqvlem  7093  marypha1lem  7202  fin23lem26  7967  axdc3lem4  8095  mulcmpblnr  8712  ltsrpr  8715  sub4  9108  muladd  9228  ltleadd  9273  divdivdiv  9477  divadddiv  9491  ltmul12a  9628  lt2mul2div  9648  xlemul1a  10624  fzrev  10862  facndiv  11317  fsumconst  12268  isprm5  12807  acsfn2  13581  ghmeql  14721  subgdmdprd  15285  lssvsubcl  15717  lssvacl  15727  lidlsubcl  15984  ocvin  16590  alexsubALTlem2  17758  alexsubALTlem3  17759  blbas  17992  nmoco  18262  cncfmet  18428  cmetcaulem  18730  mbflimsup  19037  ulmdvlem3  19795  ptolemy  19880  grpoideu  20892  ipblnfi  21450  htthlem  21513  hvaddsub4  21673  bralnfn  22544  hmops  22616  hmopm  22617  adjadd  22689  opsqrlem1  22736  atomli  22978  chirredlem2  22987  atcvat3i  22992  mdsymlem5  23003  cdj1i  23029  derangenlem  23717  dfon2lem6  24215  poseq  24324  sltsolem1  24393  prdsbnd  26620  heibor1lem  26636  congneg  27159  jm2.26  27198  lindfmm  27400  hl2at  30216
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