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

Theorem anabsi7 670
 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 669 . 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:  nelrdva  3644  elunii  4806  ordelord  6182  fvelrn  6822  onsucuni2  7532  fnfi  8783  prnmax  10409  relexpindlem  14417  opreu2reuALT  30257  ralssiun  34843  monotoddzz  39927  oddcomabszz  39928  flcidc  40161  syldbl2  40915  fmul01  42265  fprodcnlem  42284  stoweidlem4  42689  stoweidlem20  42705  stoweidlem22  42707  stoweidlem27  42712  stoweidlem30  42715  stoweidlem51  42736  stoweidlem59  42744  fourierdlem21  42813  fourierdlem89  42880  fourierdlem90  42881  fourierdlem91  42882  fourierdlem104  42895
 Copyright terms: Public domain W3C validator