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

Theorem impel 509
 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 410 1 ((𝜑𝜃) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  equs5e  2483  elabgt  3646  mob2  3691  ssn0rex  4296  reusv2lem2  5281  copsex2t  5364  reuop  6125  trssord  6189  trsuc  6256  funimass2  6418  fvelima  6712  fvmptf  6770  funfvima2  6975  funfvima3  6980  tfi  7551  suppssov1  7845  tposf2  7899  wfrlem4  7941  wfrlem10  7947  ectocld  8347  mapsnd  8433  resixpfo  8483  f1oeng  8511  nneneq  8684  nnsdomg  8761  fiint  8779  fodomfi  8781  eqinf  8932  hartogslem1  8990  cantnf  9140  rankwflemb  9206  carden2a  9379  carduni  9394  harval2  9410  cardaleph  9500  alephval3  9521  dfac5  9539  cfcof  9681  axdc4lem  9862  nqereu  10336  recexsr  10514  seqcoll  13816  swrdswrd  14056  swrdccatin1  14076  swrdccatin2  14080  repswswrd  14135  climcau  15016  odd2np1  15679  lcmfunsnlem2lem2  15970  coprmproddvdslem  15993  dvdsprm  16034  vdwlem6  16309  imasvscafn  16799  dirref  17834  irredn1  19445  isdrngd  19513  gsummoncoe1  20458  psgnghm  20710  prdstopn  22222  cnextcn  22661  tnggrpr  23250  ovolctb  24083  dyadmbl  24193  itg1addlem4  24292  itg1le  24306  dvcnp2  24512  c1liplem1  24588  pserulm  25006  perfectlem2  25803  dchrisumlem2  26063  axlowdimlem16  26740  wlkv0  27429  wlkp1lem1  27452  wlkswwlksf1o  27654  wspniunwspnon  27698  trlsegvdeglem1  27994  frcond4  28044  2clwwlk2clwwlk  28124  opabssi  30361  nn0xmulclb  30493  cusgr3cyclex  32401  satfun  32676  fundmpss  33027  frrlem4  33144  noresle  33218  nn0prpw  33689  bj-restpw  34411  bj-prmoore  34435  domalom  34723  cover2  35052  setindtr  39797  climxlim2lem  42329  2reuimp  43513  fvelsetpreimafv  43746  imasetpreimafvbijlemfo  43764  reupr  43881  lighneallem4  43970  proththd  43974  lincresunit3  44731
 Copyright terms: Public domain W3C validator