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

Theorem ad2ant2lr 747
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1
Assertion
Ref Expression
ad2ant2lr

Proof of Theorem ad2ant2lr
StepHypRef Expression
1 ad2ant2.1 . . 3
21adantrr 716 . 2
32adantll 713 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  reusv2lem2  4654  mpteqb  5970  omxpenlem  7638  fineqvlem  7754  marypha1lem  7913  fin23lem26  8726  axdc3lem4  8854  mulcmpblnr  9469  ltsrpr  9475  sub4  9887  muladd  10014  ltleadd  10060  divdivdiv  10270  divadddiv  10284  ltmul12a  10423  lt2mul2div  10446  xlemul1a  11509  fzrev  11771  facndiv  12366  fsumconst  13605  fprodconst  13782  isprm5  14253  acsfn2  15060  ghmeql  16289  subgdmdprd  17081  lssvsubcl  17590  lssvacl  17600  lidlsubclOLD  17864  ocvin  18705  lindfmm  18862  scmatghm  19035  scmatmhm  19036  slesolinv  19182  slesolinvbi  19183  slesolex  19184  pm2mpf1lem  19295  pm2mpcoe1  19301  reftr  20015  alexsubALTlem2  20548  alexsubALTlem3  20549  blbas  20933  nmoco  21244  cncfmet  21412  cmetcaulem  21727  mbflimsup  22073  ulmdvlem3  22797  ptolemy  22889  grpoideu  25211  ipblnfi  25771  htthlem  25834  hvaddsub4  25995  bralnfn  26867  hmops  26939  hmopm  26940  adjadd  27012  opsqrlem1  27059  atomli  27301  chirredlem2  27310  atcvat3i  27315  mdsymlem5  27326  cdj1i  27352  derangenlem  28615  elmrsubrn  28880  dfon2lem6  29220  poseq  29333  sltsolem1  29428  mblfinlem1  30051  prdsbnd  30289  heibor1lem  30305  congneg  30907  jm2.26  30944  stoweidlem34  31816  lindslinindsimp2  33064  aacllem  33216  hl2at  35129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator