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

Theorem anabsi5 659
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 397 . 2 ((𝜑 ∧ (𝜑𝜓)) → 𝜒)
32anabss5 658 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386
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 199  df-an 387
This theorem is referenced by:  anabsi6  660  anabsi8  662  3anidm12  1491  rspce  3506  onint  7275  f1oweALT  7431  php2  8435  hasheqf1oi  13463  rtrclreclem3  14213  rtrclreclem4  14214  ptcmpfi  22036  redwlk  27040  frgruhgr0v  27688  finxpreclem2  33829  finxpreclem6  33835  diophin  38310  diophun  38311  rspcegf  40129  stoweidlem36  41194
  Copyright terms: Public domain W3C validator