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 462 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  syldbl2  841  nelrdva  3618  elunii  4824  ordelord  6235  fvelrn  6897  onsucuni2  7613  fnfi  8858  prnmax  10609  relexpindlem  14626  opreu2reuALT  30544  ralssiun  35315  monotoddzz  40468  oddcomabszz  40469  flcidc  40702  fmul01  42796  fprodcnlem  42815  stoweidlem4  43220  stoweidlem20  43236  stoweidlem22  43238  stoweidlem27  43243  stoweidlem30  43246  stoweidlem51  43267  stoweidlem59  43275  fourierdlem21  43344  fourierdlem89  43411  fourierdlem90  43412  fourierdlem91  43413  fourierdlem104  43426
  Copyright terms: Public domain W3C validator