MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad2ant2lr Structured version   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  4725  mpteqb  5819  omxpenlem  7209  fineqvlem  7323  marypha1lem  7438  fin23lem26  8205  axdc3lem4  8333  mulcmpblnr  8949  ltsrpr  8952  sub4  9346  muladd  9466  ltleadd  9511  divdivdiv  9715  divadddiv  9729  ltmul12a  9866  lt2mul2div  9886  xlemul1a  10867  fzrev  11108  facndiv  11579  fsumconst  12573  isprm5  13112  acsfn2  13888  ghmeql  15028  subgdmdprd  15592  lssvsubcl  16020  lssvacl  16030  lidlsubcl  16287  ocvin  16901  alexsubALTlem2  18079  alexsubALTlem3  18080  blbas  18460  nmoco  18771  cncfmet  18938  cmetcaulem  19241  mbflimsup  19558  ulmdvlem3  20318  ptolemy  20404  grpoideu  21797  ipblnfi  22357  htthlem  22420  hvaddsub4  22580  bralnfn  23451  hmops  23523  hmopm  23524  adjadd  23596  opsqrlem1  23643  atomli  23885  chirredlem2  23894  atcvat3i  23899  mdsymlem5  23910  cdj1i  23936  derangenlem  24857  fprodconst  25302  dfon2lem6  25415  poseq  25528  sltsolem1  25623  mblfinlem1  26243  prdsbnd  26502  heibor1lem  26518  congneg  27034  jm2.26  27073  lindfmm  27274  stoweidlem34  27759  hl2at  30202
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