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

Theorem ad2ant2lr 729
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 698 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantll 695 1  |-  ( ( ( th  /\  ph )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  reusv2lem2  4684  mpteqb  5778  omxpenlem  7168  fineqvlem  7282  marypha1lem  7396  fin23lem26  8161  axdc3lem4  8289  mulcmpblnr  8905  ltsrpr  8908  sub4  9302  muladd  9422  ltleadd  9467  divdivdiv  9671  divadddiv  9685  ltmul12a  9822  lt2mul2div  9842  xlemul1a  10823  fzrev  11064  facndiv  11534  fsumconst  12528  isprm5  13067  acsfn2  13843  ghmeql  14983  subgdmdprd  15547  lssvsubcl  15975  lssvacl  15985  lidlsubcl  16242  ocvin  16856  alexsubALTlem2  18032  alexsubALTlem3  18033  blbas  18413  nmoco  18724  cncfmet  18891  cmetcaulem  19194  mbflimsup  19511  ulmdvlem3  20271  ptolemy  20357  grpoideu  21750  ipblnfi  22310  htthlem  22373  hvaddsub4  22533  bralnfn  23404  hmops  23476  hmopm  23477  adjadd  23549  opsqrlem1  23596  atomli  23838  chirredlem2  23847  atcvat3i  23852  mdsymlem5  23863  cdj1i  23889  derangenlem  24810  fprodconst  25255  dfon2lem6  25358  poseq  25467  sltsolem1  25536  mblfinlem  26143  prdsbnd  26392  heibor1lem  26408  congneg  26924  jm2.26  26963  lindfmm  27165  stoweidlem34  27650  hl2at  29887
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