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

Theorem anabsan2 673
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 648 . 2 ((𝜓 ∧ (𝜑𝜓)) → 𝜒)
32anabss7 672 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  anabss3  674  anandirs  678  fvreseq  6787  funcestrcsetclem7  17388  funcsetcestrclem7  17403  lmodvsdi  19650  lmodvsdir  19651  lmodvsass  19652  lss0cl  19711  phlpropd  20344  chpdmatlem3  21445  mbfimasn  24236  slmdvsdi  30893  slmdvsdir  30894  slmdvsass  30895  metider  31247  funcringcsetcALTV2lem7  44664  funcringcsetclem7ALTV  44687
  Copyright terms: Public domain W3C validator