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:  tbwlem1  1709  tbwlem2  1710  re1luk3  1716  merco1lem17  1737  re1tbw1  1749  spimew  1976  relcnvtrg  6159  relresfld  6168  onfr  6290  foimacnv  6717  fvi  6826  isoini2  7190  ovidig  7393  f1oexbi  7749  frxp  7938  smores2  8156  tfrlem5  8182  en2sn  8785  en2snOLD  8786  mapdom1  8878  php2  8898  snnen2o  8903  frfi  8989  fodomfi  9022  ixpfi2  9047  hartogs  9233  wemapsolem  9239  card2on  9243  unwdomg  9273  r1pwss  9473  tz9.12lem3  9478  uniwf  9508  rankval3b  9515  djuun  9615  tskwe  9639  carddomi2  9659  cardsdomelir  9662  infxpenlem  9700  inffien  9750  alephord  9762  alephdom  9768  iunfictbso  9801  dfac8  9822  dfacacn  9828  dfac13  9829  dfac12lem2  9831  infmap2  9905  ackbij1b  9926  ackbij2  9930  fictb  9932  cfslb  9953  fin67  10082  fin1a2lem10  10096  fin1a2lem11  10097  dcomex  10134  ttukeylem1  10196  ttukeylem7  10202  ondomon  10250  konigthlem  10255  alephadd  10264  alephexp1  10266  alephreg  10269  pwcfsdom  10270  fpwwe2lem12  10329  gchaleph  10358  gchaleph2  10359  winainflem  10380  inttsk  10461  inar1  10462  inatsk  10465  grudomon  10504  nqerid  10620  nqpr  10701  zmin  12613  uzrdgsuci  13608  isfinite4  14005  pfxccatin12lem3  14373  limsupval2  15117  sumz  15362  fsumsers  15368  isumclim  15397  ntrivcvgfvn0  15539  ntrivcvgtail  15540  zprodn0  15577  iprodclim  15636  alzdvds  15957  bitsfzolem  16069  phicl2  16397  phibnd  16400  pclem  16467  strle1  16787  fnpr2ob  17186  psss  18213  symg2bas  18915  dprdss  19547  2ndcdisj  22515  dis2ndc  22519  hausmapdom  22559  ptcnplem  22680  fbun  22899  metrest  23586  opnreen  23900  ivthle  24525  ivthle2  24526  ovolfiniun  24570  volfiniun  24616  uniiccdif  24647  uniioovol  24648  uniioombllem4  24655  dyadmbl  24669  vitali  24682  mbflimsup  24735  cpnres  25006  dvcj  25019  dvef  25049  dvne0  25080  lhop2  25084  itgparts  25116  itgsubstlem  25117  ply1divex  25206  fta1blem  25238  dgrlem  25295  pige3ALT  25581  xrlimcnp  26023  ftalem3  26129  lgsdchr  26408  2lgslem1  26447  addsqn2reu  26494  2sqreultblem  26501  2sqreunnltblem  26504  dchrvmasumlem2  26551  pntlem3  26662  tgisline  26892  axcontlem2  27236  upgrex  27365  umgrnloop2  27419  usgriedgleord  27498  uspgredgleord  27502  nbedgusgr  27642  nb3grprlem2  27651  rusgrnumwrdl2  27856  wlkp1lem2  27944  wwlksnexthasheq  28169  wlksnwwlknvbij  28174  2pthon3v  28209  umgr2wlk  28215  rusgrnumwlkg  28243  umgrclwwlkge2  28256  clwwlkvbij  28378  0pthonv  28394  1pthon2v  28418  numclwwlkqhash  28640  chscllem4  29903  adjeq  30198  hmopidmchi  30414  xreceu  31098  tocyccntz  31313  archirngz  31345  archiabllem1b  31348  locfinreflem  31692  measvuni  32082  elmbfmvol2  32134  omsmeas  32190  sibfof  32207  eulerpartlemgvv  32243  ballotlemfc0  32359  ballotlemfcc  32360  iccllysconn  33112  cvmliftphtlem  33179  satfv1  33225  sat1el2xp  33241  ttrclss  33706  opnrebl2  34437  re1ax2lem  34503  re1ax2  34504  bj-orim2  34663  bj-peircecurry  34665  lindsdom  35698  poimir  35737  volsupnfl  35749  areacirc  35797  totbndbnd  35874  islsati  36935  hdmap14lem2a  39808  rabdiophlem1  40539  pellexlem5  40571  ttac  40774  aomclem4  40798  hbtlem5  40869  idomodle  40937  idomsubgmo  40939  rp-isfinite5  41022  iscard4  41038  mnuunid  41784  vk15.4j  42037  ax6e2nd  42067  trsspwALT2  42328  sspwtrALT  42331  sstrALT2  42344  dvmptconst  43346  dvmptidg  43348  fperdvper  43350  dvmulcncf  43356  dvdivcncf  43358  fourierdlem20  43558  fouriercn  43663  ndmaovcl  44582  fundcmpsurinjpreimafv  44748  fmtnofac2  44909  prminf2  44928  isomuspgrlem2  45173  irinitoringc  45515  pgrpgt2nabl  45590  line2x  45988  prstchom2ALT  46246  spcdvw  46271  aacllem  46391