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  4535  mpteqb  5576  omxpenlem  6959  fineqvlem  7073  marypha1lem  7182  fin23lem26  7947  axdc3lem4  8075  mulcmpblnr  8692  ltsrpr  8695  sub4  9088  muladd  9208  ltleadd  9253  divdivdiv  9457  divadddiv  9471  ltmul12a  9608  lt2mul2div  9628  xlemul1a  10604  fzrev  10842  facndiv  11297  fsumconst  12248  isprm5  12787  acsfn2  13561  ghmeql  14701  subgdmdprd  15265  lssvsubcl  15697  lssvacl  15707  lidlsubcl  15964  ocvin  16570  alexsubALTlem2  17738  alexsubALTlem3  17739  blbas  17972  nmoco  18242  cncfmet  18408  cmetcaulem  18710  mbflimsup  19017  ulmdvlem3  19775  ptolemy  19860  grpoideu  20870  ipblnfi  21428  htthlem  21491  hvaddsub4  21653  bralnfn  22524  hmops  22596  hmopm  22597  adjadd  22669  opsqrlem1  22716  atomli  22958  chirredlem2  22967  atcvat3i  22972  mdsymlem5  22983  cdj1i  23009  derangenlem  23109  dfon2lem6  23548  poseq  23657  axsltsolem1  23725  prdsbnd  25928  heibor1lem  25944  congneg  26467  jm2.26  26506  lindfmm  26708  hl2at  28873
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