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  18191  funcsetcestrclem7  18206  lmodvsdi  20883  lmodvsdir  20884  lmodvsass  20885  lss0cl  20945  phlpropd  21673  chpdmatlem3  22846  mbfimasn  25667  slmdvsdi  33221  slmdvsdir  33222  slmdvsass  33223  metider  33893  funcringcsetcALTV2lem7  48212  funcringcsetclem7ALTV  48235
  Copyright terms: Public domain W3C validator