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

Theorem impel 507
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 408 1 ((𝜑𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  equs5e  2457  elabgtOLD  3626  mob2  3674  ssn0rex  4316  reusv2lem2  5355  copsex2t  5450  reuop  6246  trssord  6335  trsuc  6405  funimass2  6585  fvelima  6909  fvmptf  6970  funfvima2  7182  funfvima3  7187  tfi  7790  suppssov1  8130  tposf2  8182  frrlem4  8221  wfrlem4OLD  8259  wfrlem10OLD  8265  ectocld  8726  mapsnd  8827  resixpfo  8877  f1oeng  8914  nneneq  9156  nneneqOLD  9168  nnsdomgOLD  9250  fiint  9271  fodomfi  9272  eqinf  9425  hartogslem1  9483  cantnf  9634  rankwflemb  9734  carden2a  9907  carduni  9922  harval2  9938  cardaleph  10030  alephval3  10051  dfac5  10069  cfcof  10215  axdc4lem  10396  nqereu  10870  recexsr  11048  seqcoll  14369  swrdswrd  14599  swrdccatin1  14619  swrdccatin2  14623  repswswrd  14678  climcau  15561  odd2np1  16228  lcmfunsnlem2lem2  16520  coprmproddvdslem  16543  dvdsprm  16584  vdwlem6  16863  imasvscafn  17424  dirref  18495  irredn1  20142  isdrngd  20226  isdrngdOLD  20228  psgnghm  21000  gsummoncoe1  21691  prdstopn  22995  cnextcn  23434  tnggrpr  24035  ovolctb  24870  dyadmbl  24980  itg1addlem4  25079  itg1addlem4OLD  25080  itg1le  25094  dvcnp2  25300  c1liplem1  25376  pserulm  25797  perfectlem2  26594  dchrisumlem2  26854  noresle  27061  bday1s  27192  axlowdimlem16  27948  wlkv0  28641  wlkp1lem1  28663  wlkswwlksf1o  28866  wspniunwspnon  28910  trlsegvdeglem1  29206  frcond4  29256  2clwwlk2clwwlk  29336  opabssi  31578  nn0xmulclb  31723  zarclsiin  32509  cusgr3cyclex  33787  satfun  34062  fundmpss  34397  nn0prpw  34841  bj-restpw  35609  bj-prmoore  35632  domalom  35921  cover2  36219  disjlem18  37308  sticksstones11  40610  setindtr  41391  onov0suclim  41652  oe0suclim  41655  ofoaid1  41717  ofoaid2  41718  naddcnfcom  41725  naddcnfass  41728  climxlim2lem  44172  2reuimp  45433  fvelsetpreimafv  45665  imasetpreimafvbijlemfo  45683  reupr  45800  lighneallem4  45888  proththd  45892  lincresunit3  46648
  Copyright terms: Public domain W3C validator