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

Theorem anabsi7 670
Description: Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
Hypothesis
Ref Expression
anabsi7.1 (𝜓 → ((𝜑𝜓) → 𝜒))
Assertion
Ref Expression
anabsi7 ((𝜑𝜓) → 𝜒)

Proof of Theorem anabsi7
StepHypRef Expression
1 anabsi7.1 . . 3 (𝜓 → ((𝜑𝜓) → 𝜒))
21anabsi6 669 . 2 ((𝜓𝜑) → 𝜒)
32ancoms 460 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  syldbl2  840  nelrdva  3664  elunii  4871  ordelord  6340  fvelrn  7028  onsucuni2  7770  fnfi  9128  prnmax  10936  relexpindlem  14954  opreu2reuALT  31448  ralssiun  35924  monotoddzz  41310  oddcomabszz  41311  flcidc  41544  fmul01  43907  fprodcnlem  43926  stoweidlem4  44331  stoweidlem20  44347  stoweidlem22  44349  stoweidlem27  44354  stoweidlem30  44357  stoweidlem51  44378  stoweidlem59  44386  fourierdlem21  44455  fourierdlem89  44522  fourierdlem90  44523  fourierdlem91  44524  fourierdlem104  44537
  Copyright terms: Public domain W3C validator