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

Theorem anabsi5 854
 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 853 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 196  df-an 385 This theorem is referenced by:  anabsi6  855  anabsi8  857  3anidm12  1375  rspce  3277  onint  6887  f1oweALT  7043  php2  8030  hasheqf1oi  13002  hasheqf1oiOLD  13003  rtrclreclem3  13648  rtrclreclem4  13649  ptcmpfi  21426  redwlk  26136  vdusgraval  26434  finxpreclem2  32403  finxpreclem6  32409  diophin  36354  diophun  36355  rspcegf  38205  rspcef  38267  stoweidlem36  38929  red1wlk  40881  frgruhgr0v  41435
 Copyright terms: Public domain W3C validator