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

Theorem anabsi5 666
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 206  df-an 396
This theorem is referenced by:  anabsi6  667  anabsi8  669  3anidm12  1418  rspce  3601  onint  7782  f1oweALT  7963  php2OLD  9229  hasheqf1oi  14318  rtrclreclem3  15014  rtrclreclem4  15015  ablsimpgfindlem1  20025  ptcmpfi  23637  redwlk  29362  frgruhgr0v  29950  finxpreclem2  36735  finxpreclem6  36741  diophin  41973  diophun  41974  rspcegf  44170  stoweidlem36  45211
  Copyright terms: Public domain W3C validator