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

Theorem anabsi7 671
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 670 . 2 ((𝜓𝜑) → 𝜒)
32ancoms 458 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  syldbl2  841  nelrdva  3710  elunii  4911  ordelord  6405  fvelrn  7095  onsucuni2  7855  fnfi  9219  prnmax  11036  relexpindlem  15103  opreu2reuALT  32497  ralssiun  37409  monotoddzz  42960  oddcomabszz  42961  flcidc  43187  fmul01  45600  fprodcnlem  45619  stoweidlem4  46024  stoweidlem20  46040  stoweidlem22  46042  stoweidlem27  46047  stoweidlem30  46050  stoweidlem51  46071  stoweidlem59  46079  fourierdlem21  46148  fourierdlem89  46215  fourierdlem90  46216  fourierdlem91  46217  fourierdlem104  46230
  Copyright terms: Public domain W3C validator