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

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

Proof of Theorem 3ad2antr3
StepHypRef Expression
1 3ad2antl.1 . . 3
21adantrl 715 . 2
323adantr1 1155 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  frfi  7785  ressress  14694  latjjdir  15734  grprcan  16083  grpsubrcan  16119  grpaddsubass  16128  mhmmnd  16192  zntoslem  18595  ipdir  18674  ipass  18680  qustgpopn  20618  constr3trllem1  24650  wwlkextproplem3  24743  grpomuldivass  25251  grpopnpcan2  25255  nvmdi  25545  dmdsl3  27234  dvrcan5  27783  voliune  28201  btwnconn1lem7  29743  funcestrcsetclem9  32654  funcsetcestrclem9  32669  funcringcsetcOLD2lem9  32852  funcringcsetclem9OLD  32875  cvrnbtwn4  35004  paddasslem14  35557  paddasslem17  35560  paddss  35569  pmod1i  35572  cdleme1  35952  cdleme2  35953
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