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

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

Proof of Theorem ad2ant2rl
StepHypRef Expression
1 ad2ant2.1 . . 3
21adantrl 715 . 2
32adantlr 714 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  omwordri  7240  omxpenlem  7638  infxpabs  8613  domfin4  8712  isf32lem7  8760  ordpipq  9341  muladd  10014  lemul12b  10424  mulge0b  10437  qaddcl  11227  iooshf  11632  elfzomelpfzo  11914  expnegz  12200  bitsshft  14125  setscom  14662  catideu  15072  lubun  15753  grplmulf1o  16112  lidl1el  17866  frlmipval  18810  en2top  19487  cnpnei  19765  kgenidm  20048  ufileu  20420  fmfnfmlem4  20458  isngp4  21131  fsumcn  21374  evth  21459  mbfmulc2lem  22054  itg1addlem4  22106  dgreq0  22662  cxplt3  23081  cxple3  23082  basellem4  23357  axcontlem2  24268  usgra2adedgspth  24613  usghashecclwwlk  24835  grpoidinvlem3  25208  grpoideu  25211  grporcan  25223  3oalem2  26581  hmops  26939  adjadd  27012  mdslmd4i  27252  mdexchi  27254  mdsymlem1  27322  cvxscon  28688  poseq  29333  sltsolem1  29428  nodenselem5  29445  mblfinlem4  30054  ismblfin  30055  tailfb  30195  ismtyres  30304  ghomco  30345  rngoisocnv  30384  1idl  30423  srhmsubc  32884  srhmsubcOLD  32903  aacllem  33216  bnj607  33974  ps-2  35202
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