MPE Home 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 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  840  nelrdva  3727  elunii  4936  ordelord  6417  fvelrn  7110  onsucuni2  7870  fnfi  9244  prnmax  11064  relexpindlem  15112  opreu2reuALT  32505  ralssiun  37373  monotoddzz  42900  oddcomabszz  42901  flcidc  43131  fmul01  45501  fprodcnlem  45520  stoweidlem4  45925  stoweidlem20  45941  stoweidlem22  45943  stoweidlem27  45948  stoweidlem30  45951  stoweidlem51  45972  stoweidlem59  45980  fourierdlem21  46049  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem104  46131
  Copyright terms: Public domain W3C validator