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

Step	Hyp	Ref	Expression
1		mpsyl.1	. . 3 ⊢ 𝜑
2	1	a1i 11	. 2 ⊢ (𝜓 → 𝜑)
3		mpsyl.2	. 2 ⊢ (𝜓 → 𝜒)
4		mpsyl.3	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	2, 3, 4	sylc 65	1 ⊢ (𝜓 → 𝜃)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  spimew  1971  snssg  4747  relcnvtrg  6239  relresfld  6249  onfr  6371  foimacnv  6817  fvi  6937  isoini2  7314  ovidig  7531  f1oexbi  7904  frxp  8105  smores2  8323  tfrlem5  8348  en2sn  9012  en2prd  9019  mapdom1  9106  frfi  9232  fodomfi  9261  fodomfiOLD  9281  ixpfi2  9301  hartogs  9497  wemapsolem  9503  card2on  9507  unwdomg  9537  ttrclss  9673  r1pwss  9737  tz9.12lem3  9742  uniwf  9772  rankval3b  9779  djuun  9879  tskwe  9903  carddomi2  9923  cardsdomelir  9926  infxpenlem  9966  inffien  10016  alephord  10028  alephdom  10034  iunfictbso  10067  dfac8  10089  dfacacn  10095  dfac13  10096  dfac12lem2  10098  infmap2  10170  ackbij1b  10191  ackbij2  10195  fictb  10197  cfslb  10219  fin67  10348  fin1a2lem10  10362  fin1a2lem11  10363  dcomex  10400  ttukeylem1  10462  ttukeylem7  10468  ondomon  10516  konigthlem  10521  alephadd  10530  alephexp1  10532  alephreg  10535  pwcfsdom  10536  fpwwe2lem12  10595  gchaleph  10624  gchaleph2  10625  winainflem  10646  inttsk  10727  inar1  10728  inatsk  10731  grudomon  10770  nqerid  10886  nqpr  10967  zmin  12903  uzrdgsuci  13925  isfinite4  14327  pfxccatin12lem3  14697  limsupval2  15446  sumz  15688  fsumsers  15694  isumclim  15723  ntrivcvgfvn0  15865  ntrivcvgtail  15866  zprodn0  15905  iprodclim  15964  alzdvds  16290  bitsfzolem  16404  phicl2  16738  phibnd  16741  pclem  16809  strle1  17128  fnpr2ob  17521  psss  18539  symg2bas  19323  dprdss  19961  irinitoringc  21389  2ndcdisj  23343  dis2ndc  23347  hausmapdom  23387  ptcnplem  23508  fbun  23727  metrest  24412  opnreen  24720  ivthle  25357  ivthle2  25358  ovolfiniun  25402  volfiniun  25448  uniiccdif  25479  uniioovol  25480  uniioombllem4  25487  dyadmbl  25501  vitali  25514  mbflimsup  25567  cpnres  25839  dvcj  25854  dvef  25884  dvne0  25916  lhop2  25920  itgparts  25954  itgsubstlem  25955  ply1divex  26042  fta1blem  26076  dgrlem  26134  pige3ALT  26429  xrlimcnp  26878  ftalem3  26985  lgsdchr  27266  2lgslem1  27305  addsqn2reu  27352  2sqreultblem  27359  2sqreunnltblem  27362  dchrvmasumlem2  27409  pntlem3  27520  mulsproplem13  28031  mulsproplem14  28032  tgisline  28554  axcontlem2  28892  upgrex  29019  umgrnloop2  29073  usgriedgleord  29155  uspgredgleord  29159  nbedgusgr  29299  nb3grprlem2  29308  rusgrnumwrdl2  29514  wlkp1lem2  29602  wwlksnexthasheq  29833  wlksnwwlknvbij  29838  2pthon3v  29873  umgr2wlk  29879  rusgrnumwlkg  29907  umgrclwwlkge2  29920  clwwlkvbij  30042  0pthonv  30058  1pthon2v  30082  numclwwlkqhash  30304  chscllem4  31569  adjeq  31864  hmopidmchi  32080  xreceu  32842  tocyccntz  33101  archirngz  33143  archiabllem1b  33146  locfinreflem  33830  measvuni  34204  elmbfmvol2  34258  omsmeas  34314  sibfof  34331  eulerpartlemgvv  34367  ballotlemfc0  34484  ballotlemfcc  34485  iccllysconn  35237  cvmliftphtlem  35304  satfv1  35350  sat1el2xp  35366  opnrebl2  36309  re1ax2lem  36375  re1ax2  36376  bj-orim2  36544  bj-peircecurry  36546  lindsdom  37608  poimir  37647  volsupnfl  37659  areacirc  37707  totbndbnd  37783  islsati  38987  hdmap14lem2a  41861  rabdiophlem1  42789  pellexlem5  42821  ttac  43025  aomclem4  43046  hbtlem5  43117  idomodle  43180  idomsubgmo  43182  nnoeomeqom  43301  omabs2  43321  rp-isfinite5  43506  iscard4  43522  mnuunid  44266  vk15.4j  44518  ax6e2nd  44548  trsspwALT2  44808  sspwtrALT  44811  sstrALT2  44824  permaxrep  44996  dvmptconst  45913  dvmptidg  45915  fperdvper  45917  dvmulcncf  45923  dvdivcncf  45925  fourierdlem20  46125  fouriercn  46230  ndmaovcl  47204  fundcmpsurinjpreimafv  47409  fmtnofac2  47570  prminf2  47589  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpgprismgr4cyclex  48097  pgrpgt2nabl  48354  line2x  48743  prstchom2ALT  49553  spcdvw  49668  aacllem  49790