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

Theorem anabsi7 855
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 854 . 2 ((𝜓𝜑) → 𝜒)
32ancoms 467 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  syl2an23an  1378  nelrdva  3379  elunii  4367  ordelord  5644  fvelrn  6241  onsucuni2  6899  fnfi  8096  prnmax  9669  monotoddzz  36325  oddcomabszz  36326  flcidc  36562  syldbl2  37289  fmul01  38447  fprodcnlem  38466  stoweidlem4  38697  stoweidlem20  38713  stoweidlem22  38715  stoweidlem27  38720  stoweidlem30  38723  stoweidlem51  38744  stoweidlem59  38752  fourierdlem21  38821  fourierdlem89  38888  fourierdlem90  38889  fourierdlem91  38890  fourierdlem104  38903
  Copyright terms: Public domain W3C validator