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

Theorem mpsyl 68
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 65 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  1627  tbwlem2  1628  re1luk3  1634  merco1lem17  1655  re1tbw1  1667  relcnvtr  5624  relresfld  5631  onfr  5732  foimacnv  6121  fvi  6222  isoini2  6554  ovidig  6743  f1oexbi  7078  frxp  7247  smores2  7411  tfrlem5  7436  mapdom1  8085  php2  8105  snnen2o  8109  frfi  8165  fodomfi  8199  ixpfi2  8224  hartogs  8409  wemapsolem  8415  card2on  8419  unwdomg  8449  r1pwss  8607  tz9.12lem3  8612  uniwf  8642  rankval3b  8649  tskwe  8736  carddomi2  8756  cardsdomelir  8759  infxpenlem  8796  inffien  8846  alephord  8858  alephdom  8864  iunfictbso  8897  dfac8  8917  dfacacn  8923  dfac13  8924  dfac12lem2  8926  infmap2  9000  ackbij1b  9021  ackbij2  9025  fictb  9027  cfslb  9048  fin67  9177  fin1a2lem10  9191  fin1a2lem11  9192  dcomex  9229  ttukeylem1  9291  ttukeylem7  9297  ondomon  9345  konigthlem  9350  alephadd  9359  alephexp1  9361  alephreg  9364  pwcfsdom  9365  fpwwe2lem13  9424  gchaleph  9453  gchaleph2  9454  winainflem  9475  inttsk  9556  inar1  9557  inatsk  9560  grudomon  9599  nqerid  9715  nqpr  9796  zmin  11744  uzrdgsuci  12715  isfinite4  13109  swrdccatin12lem3  13443  limsupval2  14161  caucvgb  14360  sumz  14402  fsumsers  14408  isumclim  14435  isumnn0nn  14518  climcndslem1  14525  climcndslem2  14526  ntrivcvgfvn0  14575  ntrivcvgtail  14576  zprodn0  14613  iprodclim  14673  alzdvds  14985  bitsfzolem  15099  phicl2  15416  phibnd  15419  pclem  15486  strle1  15913  psss  17154  symg2bas  17758  dprdss  18368  2ndcdisj  21199  dis2ndc  21203  hausmapdom  21243  ptcnplem  21364  fbun  21584  metrest  22269  opnreen  22574  bndth  22697  cmetcaulem  23026  ivthle  23165  ivthle2  23166  ovolfiniun  23209  volfiniun  23255  uniiccdif  23286  uniioovol  23287  uniioombllem4  23294  dyadmbl  23308  vitali  23322  mbfdm  23335  mbflimsup  23373  itg2monolem2  23458  itg2monolem3  23459  itg2mono  23460  cpnres  23640  dvcj  23653  dvef  23681  dvne0  23712  lhop2  23716  itgparts  23748  itgsubstlem  23749  ply1divex  23834  fta1blem  23866  dgrlem  23923  pige3  24207  xrlimcnp  24629  lgambdd  24697  ftalem3  24735  lgsdchr  25014  2lgslem1  25053  dchrvmasumlem2  25121  pntlem3  25232  tgisline  25456  axcontlem2  25779  upgrex  25917  umgrnloop2  25968  usgriedgleord  26047  uspgredgleord  26051  nbedgusgr  26195  rusgrnumwrdl2  26386  wlkp1lem2  26474  wlknwwlksnbij2  26681  wlkwwlkbij2  26688  wwlksnexthasheq  26701  wlksnwwlknvbij  26706  2pthon3v  26742  umgr2wlk  26748  rusgrnumwlkg  26773  umgrclwwlksge2  26812  clwwlksbij  26820  clwwlksvbij  26822  0pthonv  26890  1pthon2v  26913  numclwlk1lem2  27119  numclwwlk1  27120  numclwwlkqhash  27122  chscllem4  28387  adjeq  28682  hmopidmchi  28898  xreceu  29457  archirngz  29570  archiabllem1b  29573  locfinreflem  29731  measvuni  30100  elmbfmvol2  30152  omsmeas  30208  sibfof  30225  eulerpartlemgvv  30261  ballotlemfc0  30377  ballotlemfcc  30378  ftc2re  30492  iccllysconn  30993  cvmliftphtlem  31060  opnrebl2  32011  re1ax2lem  32077  re1ax2  32078  bj-orim2  32236  bj-currypeirce  32239  bj-peircecurry  32240  lindsdom  33074  poimir  33113  volsupnfl  33125  areacirc  33176  totbndbnd  33259  islsati  33800  hdmap14lem2a  36678  rabdiophlem1  36884  pellexlem5  36916  ttac  37122  aomclem4  37146  hbtlem5  37218  idomodle  37294  idomsubgmo  37296  rp-isfinite5  37383  vk15.4j  38255  ax6e2nd  38295  eel0001  38466  trsspwALT2  38568  sspwtrALT  38571  sstrALT2  38592  dvmptconst  39465  dvmptidg  39467  fperdvper  39470  dvmulcncf  39477  dvdivcncf  39479  fourierdlem20  39681  fouriercn  39786  ndmaovcl  40617  fmtnofac2  40810  prminf2  40829  irinitoringc  41387  pgrpgt2nabl  41465  spcdvw  41748  aacllem  41880
  Copyright terms: Public domain W3C validator