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

Theorem anabsan2 674
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 649 . 2 ((𝜓 ∧ (𝜑𝜓)) → 𝜒)
32anabss7 673 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  anabss3  675  anandirs  679  fvreseq  7060  funcestrcsetclem7  18202  funcsetcestrclem7  18217  lmodvsdi  20900  lmodvsdir  20901  lmodvsass  20902  lss0cl  20963  phlpropd  21691  chpdmatlem3  22862  mbfimasn  25681  slmdvsdi  33204  slmdvsdir  33205  slmdvsass  33206  metider  33855  funcringcsetcALTV2lem7  48140  funcringcsetclem7ALTV  48163
  Copyright terms: Public domain W3C validator