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  3695  elunii  4837  ordelord  6207  fvelrn  6837  onsucuni2  7537  fnfi  8785  prnmax  10406  relexpindlem  14412  opreu2reuALT  30168  ralssiun  34571  monotoddzz  39420  oddcomabszz  39421  flcidc  39654  syldbl2  40399  fmul01  41741  fprodcnlem  41760  stoweidlem4  42170  stoweidlem20  42186  stoweidlem22  42188  stoweidlem27  42193  stoweidlem30  42196  stoweidlem51  42217  stoweidlem59  42225  fourierdlem21  42294  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem104  42376
  Copyright terms: Public domain W3C validator