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

Theorem anabsan2 822
Description: Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.)
Hypothesis
Ref Expression
anabsan2.1
Assertion
Ref Expression
anabsan2

Proof of Theorem anabsan2
StepHypRef Expression
1 anabsan2.1 . . 3
21an12s 801 . 2
32anabss7 821 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  anabss3  823  anandirs  831  fvreseq  5989  lmodvsdi  17535  lmodvsdir  17536  lmodvsass  17537  lss0cl  17593  phlpropd  18690  chpdmatlem3  19341  mbfimasn  22041  slmdvsdi  27758  slmdvsdir  27759  slmdvsass  27760  metider  27873  funcestrcsetclem7  32652  funcsetcestrclem7  32667  funcringcsetcOLD2lem7  32850  funcringcsetclem7OLD  32873
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