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

Theorem anabsi5 853
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 443 . 2 ((𝜑 ∧ (𝜑𝜓)) → 𝜒)
32anabss5 852 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  anabsi6  854  anabsi8  856  3anidm12  1374  rspce  3276  onint  6864  f1oweALT  7020  php2  8007  hasheqf1oi  12954  hasheqf1oiOLD  12955  rtrclreclem3  13594  rtrclreclem4  13595  ptcmpfi  21368  redwlk  25902  vdusgraval  26200  finxpreclem2  32206  finxpreclem6  32212  diophin  36157  diophun  36158  rspcegf  38008  rspcef  38070  stoweidlem36  38733  red1wlk  40883  frgruhgr0v  41437
  Copyright terms: Public domain W3C validator