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  4716  mpteqb  5810  omxpenlem  7200  fineqvlem  7314  marypha1lem  7429  fin23lem26  8194  axdc3lem4  8322  mulcmpblnr  8938  ltsrpr  8941  sub4  9335  muladd  9455  ltleadd  9500  divdivdiv  9704  divadddiv  9718  ltmul12a  9855  lt2mul2div  9875  xlemul1a  10856  fzrev  11097  facndiv  11567  fsumconst  12561  isprm5  13100  acsfn2  13876  ghmeql  15016  subgdmdprd  15580  lssvsubcl  16008  lssvacl  16018  lidlsubcl  16275  ocvin  16889  alexsubALTlem2  18067  alexsubALTlem3  18068  blbas  18448  nmoco  18759  cncfmet  18926  cmetcaulem  19229  mbflimsup  19546  ulmdvlem3  20306  ptolemy  20392  grpoideu  21785  ipblnfi  22345  htthlem  22408  hvaddsub4  22568  bralnfn  23439  hmops  23511  hmopm  23512  adjadd  23584  opsqrlem1  23631  atomli  23873  chirredlem2  23882  atcvat3i  23887  mdsymlem5  23898  cdj1i  23924  derangenlem  24845  fprodconst  25291  dfon2lem6  25399  poseq  25508  sltsolem1  25577  mblfinlem  26190  prdsbnd  26439  heibor1lem  26455  congneg  26971  jm2.26  27010  lindfmm  27212  stoweidlem34  27697  hl2at  30041
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