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  4639  mpteqb  5721  omxpenlem  7106  fineqvlem  7220  marypha1lem  7333  fin23lem26  8098  axdc3lem4  8226  mulcmpblnr  8843  ltsrpr  8846  sub4  9239  muladd  9359  ltleadd  9404  divdivdiv  9608  divadddiv  9622  ltmul12a  9759  lt2mul2div  9779  xlemul1a  10760  fzrev  10999  facndiv  11466  fsumconst  12460  isprm5  12999  acsfn2  13775  ghmeql  14915  subgdmdprd  15479  lssvsubcl  15911  lssvacl  15921  lidlsubcl  16178  ocvin  16791  alexsubALTlem2  17955  alexsubALTlem3  17956  blbas  18189  nmoco  18459  cncfmet  18626  cmetcaulem  18929  mbflimsup  19236  ulmdvlem3  19996  ptolemy  20082  grpoideu  21187  ipblnfi  21747  htthlem  21810  hvaddsub4  21970  bralnfn  22841  hmops  22913  hmopm  22914  adjadd  22986  opsqrlem1  23033  atomli  23275  chirredlem2  23284  atcvat3i  23289  mdsymlem5  23300  cdj1i  23326  derangenlem  24305  fprodconst  24786  dfon2lem6  24885  poseq  24994  sltsolem1  25063  prdsbnd  26023  heibor1lem  26039  congneg  26562  jm2.26  26601  lindfmm  26803  hl2at  29665
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