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

Theorem impel 485
 Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)
Hypotheses
Ref Expression
impel.1 (𝜑 → (𝜓𝜒))
impel.2 (𝜃𝜓)
Assertion
Ref Expression
impel ((𝜑𝜃) → 𝜒)

Proof of Theorem impel
StepHypRef Expression
1 impel.2 . . 3 (𝜃𝜓)
2 impel.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5 34 . 2 (𝜑 → (𝜃𝜒))
43imp 445 1 ((𝜑𝜃) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  equs5e  2347  elabgt  3341  mob2  3380  ssn0rex  3928  reusv2lem2  4860  copsex2t  4947  trssord  5728  trsuc  5798  ectocld  7799  fiint  8222  eqinf  8375  lcmfunsnlem2lem2  15333  tnggrpr  22440  wlkv0  26528  wlkp1lem1  26551  wlkpwwlkf1ouspgr  26746  wspniunwspnon  26800  wwlksext2clwwlk  26904  trlsegvdeglem1  27060  frcond4  27114  noresle  31820  bj-restpw  33020  cover2  33479  setindtr  37410  lighneallem4  41292  proththd  41296
 Copyright terms: Public domain W3C validator