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

Theorem mpsyl 65
Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)
Hypotheses
Ref Expression
mpsyl.1 𝜑
mpsyl.2 (𝜓𝜒)
mpsyl.3 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
mpsyl (𝜓𝜃)

Proof of Theorem mpsyl
StepHypRef Expression
1 mpsyl.1 . . 3 𝜑
21a1i 11 . 2 (𝜓𝜑)
3 mpsyl.2 . 2 (𝜓𝜒)
4 mpsyl.3 . 2 (𝜑 → (𝜒𝜃))
52, 3, 4sylc 62 1 (𝜓𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  tbwlem1  1620  tbwlem2  1621  re1luk3  1627  merco1lem17  1648  re1tbw1  1660  relcnvtr  5558  relresfld  5565  onfr  5666  foimacnv  6052  fvi  6150  isoini2  6467  ovidig  6654  f1oexbi  6986  frxp  7151  smores2  7315  tfrlem5  7340  mapdom1  7987  php2  8007  snnen2o  8011  frfi  8067  fodomfi  8101  ixpfi2  8124  hartogs  8309  wemapsolem  8315  card2on  8319  unwdomg  8349  r1pwss  8507  tz9.12lem3  8512  uniwf  8542  rankval3b  8549  tskwe  8636  carddomi2  8656  cardsdomelir  8659  infxpenlem  8696  inffien  8746  alephord  8758  alephdom  8764  iunfictbso  8797  dfac8  8817  dfacacn  8823  dfac13  8824  dfac12lem2  8826  infmap2  8900  ackbij1b  8921  ackbij2  8925  fictb  8927  cfslb  8948  fin67  9077  fin1a2lem10  9091  fin1a2lem11  9092  dcomex  9129  ttukeylem1  9191  ttukeylem7  9197  ondomon  9241  konigthlem  9246  alephadd  9255  alephexp1  9257  alephreg  9260  pwcfsdom  9261  fpwwe2lem13  9320  gchaleph  9349  gchaleph2  9350  winainflem  9371  inttsk  9452  inar1  9453  inatsk  9456  grudomon  9495  nqerid  9611  nqpr  9692  zmin  11616  uzrdgsuci  12576  isfinite4  12966  swrdccatin12lem3  13287  limsupval2  14005  caucvgb  14204  sumz  14246  fsumsers  14252  isumclim  14276  isumnn0nn  14359  climcndslem1  14366  climcndslem2  14367  ntrivcvgfvn0  14416  ntrivcvgtail  14417  zprodn0  14454  iprodclim  14514  alzdvds  14826  bitsfzolem  14940  phicl2  15257  phibnd  15260  pclem  15327  strle1  15746  psss  16983  symg2bas  17587  dprdss  18197  2ndcdisj  21011  dis2ndc  21015  hausmapdom  21055  ptcnplem  21176  fbun  21396  metrest  22080  opnreen  22374  bndth  22496  cmetcaulem  22812  ivthle  22949  ivthle2  22950  ovolfiniun  22993  volfiniun  23039  uniiccdif  23069  uniioovol  23070  uniioombllem4  23077  dyadmbl  23091  vitali  23105  mbfdm  23118  mbflimsup  23156  itg2monolem2  23241  itg2monolem3  23242  itg2mono  23243  cpnres  23423  dvcj  23436  dvef  23464  dvne0  23495  lhop2  23499  itgparts  23531  itgsubstlem  23532  ply1divex  23617  fta1blem  23649  dgrlem  23706  pige3  23990  xrlimcnp  24412  lgambdd  24480  ftalem3  24518  lgsdchr  24797  2lgslem1  24836  dchrvmasumlem2  24904  pntlem3  25015  tgisline  25240  axcontlem2  25563  umgraex  25618  2trllemE  25849  0pthonv  25877  1pthon2v  25889  2pthon3v  25900  usg2wlk  25911  usg2wlkon  25912  wlknwwlknbij2  26008  wlkiswwlkbij2  26015  wwlkexthasheq  26028  wlknwwlknvbij  26034  clwwlkgt0  26065  clwwlkbij  26093  clwwlkvbij  26095  rusgrasn  26238  rusgranumwlklem4  26245  rusgranumwwlkg  26252  numclwlk1lem2  26390  numclwwlk1  26391  numclwwlkqhash  26393  chscllem4  27689  adjeq  27984  hmopidmchi  28200  xreceu  28767  archirngz  28880  archiabllem1b  28883  locfinreflem  29041  measvuni  29410  elmbfmvol2  29462  omsmeas  29518  sibfof  29535  eulerpartlemgvv  29571  ballotlemfc0  29687  ballotlemfcc  29688  iccllyscon  30292  cvmliftphtlem  30359  opnrebl2  31292  re1ax2lem  31358  re1ax2  31359  bj-orim2  31517  bj-currypeirce  31520  bj-peircecurry  31521  lindsdom  32369  poimir  32408  volsupnfl  32420  areacirc  32471  totbndbnd  32554  islsati  33095  hdmap14lem2a  35973  rabdiophlem1  36179  pellexlem5  36211  ttac  36417  aomclem4  36441  hbtlem5  36513  idomodle  36589  idomsubgmo  36591  rp-isfinite5  36678  vk15.4j  37551  ax6e2nd  37591  eel0001  37762  trsspwALT2  37864  sspwtrALT  37867  sstrALT2  37888  dvmptconst  38600  dvmptidg  38602  fperdvper  38605  dvmulcncf  38612  dvdivcncf  38614  fourierdlem20  38817  fouriercn  38922  ndmaovcl  39730  fmtnofac2  39817  prminf2  39836  upgrex  40313  umgrnloop2  40371  usgredgleord  40450  uspgredgaleord  40454  nbedgusgr  40595  rusgrnumwrdl2  40781  1wlkp1lem2  40878  wlknwwlksnbij2  41084  wlkwwlkbij2  41091  wwlksnexthasheq  41104  wlksnwwlknvbij  41109  2pthon3v-av  41145  umgr2wlk  41151  rusgrnumwlkg  41175  umgrclwwlksge2  41214  clwwlksbij  41222  clwwlksvbij  41224  0pthonv-av  41292  1pthon2v-av  41315  av-numclwlk1lem2  41522  av-numclwwlk1  41523  av-numclwwlkqhash  41525  irinitoringc  41856  pgrpgt2nabl  41936  aacllem  42312
  Copyright terms: Public domain W3C validator