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

Theorem 3ad2antr1 1161
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1
Assertion
Ref Expression
3ad2antr1

Proof of Theorem 3ad2antr1
StepHypRef Expression
1 3ad2antl.1 . . 3
21adantrr 716 . 2
323adantr3 1157 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  ispod  4813  dfwe2  6617  poxp  6912  cfcoflem  8673  axdc3lem  8851  fzosubel2  11876  sqr0lem  13074  iscatd2  15078  curf2cl  15500  yonedalem4c  15546  grpsubadd  16126  mulgnnass  16170  mulgnn0ass  16171  dprdss  17076  dprd2da  17091  srgi  17163  lsssn0  17594  psrbaglesupp  18017  psrbaglesuppOLD  18018  zntoslem  18595  blsscls  21010  iimulcl  21437  pi1grplem  21549  pi1xfrf  21553  dvconst  22320  logexprlim  23500  constr3trllem1  24650  wwlknextbi  24725  nvss  25486  disjdsct  27521  issgon  28123  measdivcstOLD  28195  measdivcst  28196  elmrsubrn  28880  ftc1anc  30098  fzadd2  30234  fdc  30238  funcestrcsetclem9  32654  funcsetcestrclem9  32669  lidldomnnring  32736  funcringcsetcOLD2lem9  32852  funcringcsetclem9OLD  32875  lincresunit3lem2  33081  cvrnbtwn3  35001  paddasslem9  35552  paddasslem17  35560  pmapjlln1  35579  lautj  35817  lautm  35818
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  df-3an 975
  Copyright terms: Public domain W3C validator