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  3702  elunii  4914  ordelord  6387  fvelrn  7079  onsucuni2  7822  fnfi  9181  prnmax  10990  relexpindlem  15010  opreu2reuALT  31748  ralssiun  36336  monotoddzz  41730  oddcomabszz  41731  flcidc  41964  fmul01  44344  fprodcnlem  44363  stoweidlem4  44768  stoweidlem20  44784  stoweidlem22  44786  stoweidlem27  44791  stoweidlem30  44794  stoweidlem51  44815  stoweidlem59  44823  fourierdlem21  44892  fourierdlem89  44959  fourierdlem90  44960  fourierdlem91  44961  fourierdlem104  44974
  Copyright terms: Public domain W3C validator