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

Theorem impel 502
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 396 1 ((𝜑𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  equs5e  2465  elabgt  3536  mob2  3581  ssn0rex  4135  reusv2lem2  5068  copsex2t  5146  trssord  5957  trsuc  6024  wfrlem4  7655  ectocld  8051  fiint  8478  eqinf  8631  lcmfunsnlem2lem2  15684  gsummoncoe1  19993  tnggrpr  22784  wlkv0  26893  wlkp1lem1  26919  wlkswwlksf1o  27129  wspniunwspnon  27205  wwlksext2clwwlkOLD  27367  trlsegvdeglem1  27558  frcond4  27612  2clwwlk2clwwlk  27697  2clwwlk2clwwlkOLD  27698  opabssi  29935  frrlem4  32289  noresle  32352  bj-restpw  33531  cnfinltrel  33732  cover2  33989  setindtr  38365  climxlim2lem  40804  lighneallem4  42298  proththd  42302
  Copyright terms: Public domain W3C validator