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

Theorem anabsi5 668
 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 486 . 2 ((𝜑𝜓) → 𝜑)
2 anabsi5.1 . 2 (𝜑 → ((𝜑𝜓) → 𝜒))
31, 2mpcom 38 1 ((𝜑𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  anabsi6  669  anabsi8  671  3anidm12  1416  rspce  3598  onint  7504  f1oweALT  7668  php2  8699  hasheqf1oi  13717  rtrclreclem3  14419  rtrclreclem4  14420  ablsimpgfindlem1  19229  ptcmpfi  22421  redwlk  27465  frgruhgr0v  28052  finxpreclem2  34752  finxpreclem6  34758  diophin  39629  diophun  39630  rspcegf  41572  stoweidlem36  42604
 Copyright terms: Public domain W3C validator