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  1707  tbwlem2  1708  re1luk3  1714  merco1lem17  1735  re1tbw1  1747  spimew  1974  relcnvtrg  6086  relresfld  6095  onfr  6198  foimacnv  6607  fvi  6715  isoini2  7071  ovidig  7271  f1oexbi  7615  frxp  7803  smores2  7974  tfrlem5  7999  mapdom1  8666  php2  8686  snnen2o  8691  frfi  8747  fodomfi  8781  ixpfi2  8806  hartogs  8992  wemapsolem  8998  card2on  9002  unwdomg  9032  r1pwss  9197  tz9.12lem3  9202  uniwf  9232  rankval3b  9239  djuun  9339  tskwe  9363  carddomi2  9383  cardsdomelir  9386  infxpenlem  9424  inffien  9474  alephord  9486  alephdom  9492  iunfictbso  9525  dfac8  9546  dfacacn  9552  dfac13  9553  dfac12lem2  9555  infmap2  9629  ackbij1b  9650  ackbij2  9654  fictb  9656  cfslb  9677  fin67  9806  fin1a2lem10  9820  fin1a2lem11  9821  dcomex  9858  ttukeylem1  9920  ttukeylem7  9926  ondomon  9974  konigthlem  9979  alephadd  9988  alephexp1  9990  alephreg  9993  pwcfsdom  9994  fpwwe2lem13  10053  gchaleph  10082  gchaleph2  10083  winainflem  10104  inttsk  10185  inar1  10186  inatsk  10189  grudomon  10228  nqerid  10344  nqpr  10425  zmin  12332  uzrdgsuci  13323  isfinite4  13719  pfxccatin12lem3  14085  limsupval2  14829  sumz  15071  fsumsers  15077  isumclim  15104  ntrivcvgfvn0  15247  ntrivcvgtail  15248  zprodn0  15285  iprodclim  15344  alzdvds  15662  bitsfzolem  15773  phicl2  16095  phibnd  16098  pclem  16165  strle1  16584  fnpr2ob  16823  psss  17816  symg2bas  18513  dprdss  19144  2ndcdisj  22061  dis2ndc  22065  hausmapdom  22105  ptcnplem  22226  fbun  22445  metrest  23131  opnreen  23436  ivthle  24060  ivthle2  24061  ovolfiniun  24105  volfiniun  24151  uniiccdif  24182  uniioovol  24183  uniioombllem4  24190  dyadmbl  24204  vitali  24217  mbflimsup  24270  cpnres  24540  dvcj  24553  dvef  24583  dvne0  24614  lhop2  24618  itgparts  24650  itgsubstlem  24651  ply1divex  24737  fta1blem  24769  dgrlem  24826  pige3ALT  25112  xrlimcnp  25554  ftalem3  25660  lgsdchr  25939  2lgslem1  25978  addsqn2reu  26025  2sqreultblem  26032  2sqreunnltblem  26035  dchrvmasumlem2  26082  pntlem3  26193  tgisline  26421  axcontlem2  26759  upgrex  26885  umgrnloop2  26939  usgriedgleord  27018  uspgredgleord  27022  nbedgusgr  27162  nb3grprlem2  27171  rusgrnumwrdl2  27376  wlkp1lem2  27464  wwlksnexthasheq  27689  wlksnwwlknvbij  27694  2pthon3v  27729  umgr2wlk  27735  rusgrnumwlkg  27763  umgrclwwlkge2  27776  clwwlkvbij  27898  0pthonv  27914  1pthon2v  27938  numclwwlkqhash  28160  chscllem4  29423  adjeq  29718  hmopidmchi  29934  xreceu  30624  tocyccntz  30836  archirngz  30868  archiabllem1b  30871  locfinreflem  31193  measvuni  31583  elmbfmvol2  31635  omsmeas  31691  sibfof  31708  eulerpartlemgvv  31744  ballotlemfc0  31860  ballotlemfcc  31861  iccllysconn  32610  cvmliftphtlem  32677  satfv1  32723  sat1el2xp  32739  opnrebl2  33782  re1ax2lem  33848  re1ax2  33849  bj-orim2  34004  bj-peircecurry  34006  lindsdom  35051  poimir  35090  volsupnfl  35102  areacirc  35150  totbndbnd  35227  islsati  36290  hdmap14lem2a  39163  rabdiophlem1  39742  pellexlem5  39774  ttac  39977  aomclem4  40001  hbtlem5  40072  idomodle  40140  idomsubgmo  40142  rp-isfinite5  40225  iscard4  40241  mnuunid  40985  vk15.4j  41234  ax6e2nd  41264  trsspwALT2  41525  sspwtrALT  41528  sstrALT2  41541  dvmptconst  42557  dvmptidg  42559  fperdvper  42561  dvmulcncf  42567  dvdivcncf  42569  fourierdlem20  42769  fouriercn  42874  ndmaovcl  43759  fundcmpsurinjpreimafv  43925  fmtnofac2  44086  prminf2  44105  isomuspgrlem2  44351  irinitoringc  44693  pgrpgt2nabl  44768  line2x  45168  spcdvw  45209  aacllem  45329