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

Theorem anabsan2 898
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 878 . 2 ((𝜓 ∧ (𝜑𝜓)) → 𝜒)
32anabss7 897 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  anabss3  899  anandirs  909  fvreseq  6434  funcestrcsetclem7  16908  funcsetcestrclem7  16923  lmodvsdi  19009  lmodvsdir  19010  lmodvsass  19011  lss0cl  19070  phlpropd  20123  chpdmatlem3  20768  mbfimasn  23521  slmdvsdi  29998  slmdvsdir  29999  slmdvsass  30000  metider  30167  funcringcsetcALTV2lem7  42469  funcringcsetclem7ALTV  42492
  Copyright terms: Public domain W3C validator