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

Theorem anabsi5 669
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 simpl 482 . 2 ((𝜑𝜓) → 𝜑)
2 anabsi5.1 . 2 (𝜑 → ((𝜑𝜓) → 𝜒))
31, 2mpcom 38 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:  anabsi6  670  anabsi8  672  3anidm12  1421  rspce  3611  onint  7810  f1oweALT  7997  php2OLD  9260  hasheqf1oi  14390  rtrclreclem3  15099  rtrclreclem4  15100  ablsimpgfindlem1  20127  ptcmpfi  23821  redwlk  29690  frgruhgr0v  30283  finxpreclem2  37391  finxpreclem6  37397  diophin  42783  diophun  42784  rspcegf  45028  stoweidlem36  46051  grlimgrtri  47963
  Copyright terms: Public domain W3C validator