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

Theorem anabsi5 893
Description: Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
Hypothesis
Ref Expression
anabsi5.1 (𝜑 → ((𝜑𝜓) → 𝜒))
Assertion
Ref Expression
anabsi5 ((𝜑𝜓) → 𝜒)

Proof of Theorem anabsi5
StepHypRef Expression
1 anabsi5.1 . . 3 (𝜑 → ((𝜑𝜓) → 𝜒))
21imp 444 . 2 ((𝜑 ∧ (𝜑𝜓)) → 𝜒)
32anabss5 892 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  anabsi6  894  anabsi8  896  3anidm12  1530  rspce  3444  onint  7160  f1oweALT  7317  php2  8310  hasheqf1oi  13334  rtrclreclem3  13999  rtrclreclem4  14000  ptcmpfi  21818  redwlk  26779  frgruhgr0v  27417  finxpreclem2  33538  finxpreclem6  33544  diophin  37838  diophun  37839  rspcegf  39681  stoweidlem36  40756
  Copyright terms: Public domain W3C validator