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  1785  tbwlem2  1786  re1luk3  1792  merco1lem17  1813  re1tbw1  1825  relcnvtr  5876  relresfld  5883  onfr  5982  foimacnv  6373  fvi  6479  isoini2  6816  ovidig  7011  f1oexbi  7349  frxp  7524  smores2  7690  tfrlem5  7715  mapdom1  8367  php2  8387  snnen2o  8391  frfi  8447  fodomfi  8481  ixpfi2  8506  hartogs  8691  wemapsolem  8697  card2on  8701  unwdomg  8731  r1pwss  8897  tz9.12lem3  8902  uniwf  8932  rankval3b  8939  djuun  9038  tskwe  9062  carddomi2  9082  cardsdomelir  9085  infxpenlem  9122  inffien  9172  alephord  9184  alephdom  9190  iunfictbso  9223  dfac8  9245  dfacacn  9251  dfac13  9252  dfac12lem2  9254  infmap2  9328  ackbij1b  9349  ackbij2  9353  fictb  9355  cfslb  9376  fin67  9505  fin1a2lem10  9519  fin1a2lem11  9520  dcomex  9557  ttukeylem1  9619  ttukeylem7  9625  ondomon  9673  konigthlem  9678  alephadd  9687  alephexp1  9689  alephreg  9692  pwcfsdom  9693  fpwwe2lem13  9752  gchaleph  9781  gchaleph2  9782  winainflem  9803  inttsk  9884  inar1  9885  inatsk  9888  grudomon  9927  nqerid  10043  nqpr  10124  zmin  12006  uzrdgsuci  12986  isfinite4  13374  swrdccatin12lem3  13717  limsupval2  14437  sumz  14679  fsumsers  14685  isumclim  14714  ntrivcvgfvn0  14855  ntrivcvgtail  14856  zprodn0  14893  iprodclim  14952  alzdvds  15268  bitsfzolem  15378  phicl2  15693  phibnd  15696  pclem  15763  strle1  16187  psss  17422  symg2bas  18022  dprdss  18633  2ndcdisj  21477  dis2ndc  21481  hausmapdom  21521  ptcnplem  21642  fbun  21861  metrest  22546  opnreen  22851  ivthle  23443  ivthle2  23444  ovolfiniun  23488  volfiniun  23534  uniiccdif  23565  uniioovol  23566  uniioombllem4  23573  dyadmbl  23587  vitali  23600  mbflimsup  23653  cpnres  23920  dvcj  23933  dvef  23963  dvne0  23994  lhop2  23998  itgparts  24030  itgsubstlem  24031  ply1divex  24116  fta1blem  24148  dgrlem  24205  pige3  24490  xrlimcnp  24915  ftalem3  25021  lgsdchr  25300  2lgslem1  25339  dchrvmasumlem2  25407  pntlem3  25518  tgisline  25742  axcontlem2  26065  upgrex  26207  umgrnloop2  26262  usgriedgleord  26341  uspgredgleord  26346  nbedgusgr  26496  nb3grprlem2  26505  rusgrnumwrdl2  26716  wlkp1lem2  26805  wlknwwlksnbij2OLD  27026  wlkwwlkbij2OLD  27033  wwlksnexthasheq  27046  wlksnwwlknvbij  27051  wlksnwwlknvbijOLD  27052  2pthon3v  27089  umgr2wlk  27095  rusgrnumwlkg  27125  umgrclwwlkge2  27140  clwwlkvbij  27288  clwwlkvbijOLDOLD  27289  clwwlkvbijOLD  27290  0pthonv  27308  1pthon2v  27332  numclwwlk1lem2OLD  27546  numclwwlkqhash  27561  chscllem4  28833  adjeq  29128  hmopidmchi  29344  xreceu  29961  archirngz  30074  archiabllem1b  30077  locfinreflem  30238  measvuni  30608  elmbfmvol2  30660  omsmeas  30716  sibfof  30733  eulerpartlemgvv  30769  ballotlemfc0  30885  ballotlemfcc  30886  iccllysconn  31560  cvmliftphtlem  31627  opnrebl2  32642  re1ax2lem  32708  re1ax2  32709  bj-orim2  32862  bj-currypeirce  32865  bj-peircecurry  32866  lindsdom  33718  poimir  33757  volsupnfl  33769  areacirc  33819  totbndbnd  33901  islsati  34776  hdmap14lem2a  37649  rabdiophlem1  37868  pellexlem5  37900  ttac  38105  aomclem4  38129  hbtlem5  38200  idomodle  38276  idomsubgmo  38278  rp-isfinite5  38364  vk15.4j  39233  ax6e2nd  39273  eel0001  39444  trsspwALT2  39544  sspwtrALT  39547  sstrALT2  39565  dvmptconst  40610  dvmptidg  40612  fperdvper  40614  dvmulcncf  40621  dvdivcncf  40623  fourierdlem20  40824  fouriercn  40929  ndmaovcl  41793  fmtnofac2  42057  prminf2  42076  irinitoringc  42638  pgrpgt2nabl  42716  spcdvw  42995  aacllem  43119