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

Theorem anabsi7 877
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 876 . 2 ((𝜓𝜑) → 𝜒)
32ancoms 468 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:  syl2an23an  1427  nelrdva  3450  elunii  4473  ordelord  5783  fvelrn  6392  onsucuni2  7076  fnfi  8279  prnmax  9855  monotoddzz  37825  oddcomabszz  37826  flcidc  38061  syldbl2  38785  fmul01  40130  fprodcnlem  40149  stoweidlem4  40539  stoweidlem20  40555  stoweidlem22  40557  stoweidlem27  40562  stoweidlem30  40565  stoweidlem51  40586  stoweidlem59  40594  fourierdlem21  40663  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem104  40745
  Copyright terms: Public domain W3C validator