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

Theorem anabsi7 667
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 666 . 2 ((𝜓𝜑) → 𝜒)
32ancoms 459 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:  nelrdva  3693  elunii  4835  ordelord  6206  fvelrn  6836  onsucuni2  7538  fnfi  8784  prnmax  10405  relexpindlem  14410  opreu2reuALT  30167  ralssiun  34570  monotoddzz  39418  oddcomabszz  39419  flcidc  39652  syldbl2  40397  fmul01  41737  fprodcnlem  41756  stoweidlem4  42166  stoweidlem20  42182  stoweidlem22  42184  stoweidlem27  42189  stoweidlem30  42192  stoweidlem51  42213  stoweidlem59  42221  fourierdlem21  42290  fourierdlem89  42357  fourierdlem90  42358  fourierdlem91  42359  fourierdlem104  42372
  Copyright terms: Public domain W3C validator