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

Theorem anabsan2 670
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 645 . 2 ((𝜓 ∧ (𝜑𝜓)) → 𝜒)
32anabss7 669 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  anabss3  671  anandirs  675  fvreseq  6802  funcestrcsetclem7  17384  funcsetcestrclem7  17399  lmodvsdi  19586  lmodvsdir  19587  lmodvsass  19588  lss0cl  19647  phlpropd  20727  chpdmatlem3  21376  mbfimasn  24160  slmdvsdi  30770  slmdvsdir  30771  slmdvsass  30772  metider  31033  funcringcsetcALTV2lem7  44241  funcringcsetclem7ALTV  44264
  Copyright terms: Public domain W3C validator