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  4665  mpteqb  5758  omxpenlem  7145  fineqvlem  7259  marypha1lem  7373  fin23lem26  8138  axdc3lem4  8266  mulcmpblnr  8882  ltsrpr  8885  sub4  9278  muladd  9398  ltleadd  9443  divdivdiv  9647  divadddiv  9661  ltmul12a  9798  lt2mul2div  9818  xlemul1a  10799  fzrev  11039  facndiv  11506  fsumconst  12500  isprm5  13039  acsfn2  13815  ghmeql  14955  subgdmdprd  15519  lssvsubcl  15947  lssvacl  15957  lidlsubcl  16214  ocvin  16824  alexsubALTlem2  18000  alexsubALTlem3  18001  blbas  18350  nmoco  18642  cncfmet  18809  cmetcaulem  19112  mbflimsup  19425  ulmdvlem3  20185  ptolemy  20271  grpoideu  21645  ipblnfi  22205  htthlem  22268  hvaddsub4  22428  bralnfn  23299  hmops  23371  hmopm  23372  adjadd  23444  opsqrlem1  23491  atomli  23733  chirredlem2  23742  atcvat3i  23747  mdsymlem5  23758  cdj1i  23784  derangenlem  24636  fprodconst  25081  dfon2lem6  25168  poseq  25277  sltsolem1  25346  prdsbnd  26193  heibor1lem  26209  congneg  26725  jm2.26  26764  lindfmm  26966  stoweidlem34  27451  hl2at  29519
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