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

Theorem anabsan2 880
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 860 . 2 ((𝜓 ∧ (𝜑𝜓)) → 𝜒)
32anabss7 879 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  881  anandirs  891  fvreseq  6359  funcestrcsetclem7  16833  funcsetcestrclem7  16848  lmodvsdi  18934  lmodvsdir  18935  lmodvsass  18936  lss0cl  18995  phlpropd  20048  chpdmatlem3  20693  mbfimasn  23446  slmdvsdi  29896  slmdvsdir  29897  slmdvsass  29898  metider  30065  funcringcsetcALTV2lem7  42367  funcringcsetclem7ALTV  42390
  Copyright terms: Public domain W3C validator