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

Theorem impel 484
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 444 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:  equs5e  2377  elabgt  3379  mob2  3419  ssn0rex  3969  reusv2lem2  4899  copsex2t  4986  trssord  5778  trsuc  5848  ectocld  7857  fiint  8278  eqinf  8431  lcmfunsnlem2lem2  15399  tnggrpr  22506  wlkv0  26603  wlkp1lem1  26626  wlkpwwlkf1ouspgr  26833  wspniunwspnon  26888  wwlksext2clwwlkOLD  27022  trlsegvdeglem1  27198  frcond4  27250  2clwwlk2clwwlk  27338  opabssi  29551  frrlem4  31908  noresle  31971  bj-restpw  33170  cover2  33638  setindtr  37908  climxlim2lem  40389  lighneallem4  41852  proththd  41856
  Copyright terms: Public domain W3C validator