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  1418  rspce  3611  onint  7810  f1oweALT  7996  php2OLD  9258  hasheqf1oi  14387  rtrclreclem3  15096  rtrclreclem4  15097  ablsimpgfindlem1  20142  ptcmpfi  23837  redwlk  29705  frgruhgr0v  30293  finxpreclem2  37373  finxpreclem6  37379  diophin  42760  diophun  42761  rspcegf  44961  stoweidlem36  45992  grlimgrtri  47899
  Copyright terms: Public domain W3C validator