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

Theorem anabsi5 893
 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 444 . 2 ((𝜑 ∧ (𝜑𝜓)) → 𝜒)
32anabss5 892 1 ((𝜑𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  anabsi6  894  anabsi8  896  3anidm12  1530  rspce  3445  onint  7162  f1oweALT  7319  php2  8313  hasheqf1oi  13355  rtrclreclem3  14020  rtrclreclem4  14021  ptcmpfi  21839  redwlk  26801  frgruhgr0v  27439  finxpreclem2  33557  finxpreclem6  33563  diophin  37857  diophun  37858  rspcegf  39700  stoweidlem36  40775
 Copyright terms: Public domain W3C validator