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

Theorem anabsi7 859
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 858 . 2 ((𝜓𝜑) → 𝜒)
32ancoms 469 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  syl2an23an  1384  nelrdva  3404  elunii  4414  ordelord  5714  fvelrn  6318  onsucuni2  6996  fnfi  8198  prnmax  9777  monotoddzz  37027  oddcomabszz  37028  flcidc  37264  syldbl2  37989  fmul01  39248  fprodcnlem  39267  stoweidlem4  39558  stoweidlem20  39574  stoweidlem22  39576  stoweidlem27  39581  stoweidlem30  39584  stoweidlem51  39605  stoweidlem59  39613  fourierdlem21  39682  fourierdlem89  39749  fourierdlem90  39750  fourierdlem91  39751  fourierdlem104  39764
  Copyright terms: Public domain W3C validator