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  1713  tbwlem2  1714  re1luk3  1720  merco1lem17  1741  re1tbw1  1753  spimew  1980  relcnvtrg  6130  relresfld  6139  onfr  6252  foimacnv  6678  fvi  6787  isoini2  7148  ovidig  7351  f1oexbi  7706  frxp  7893  smores2  8091  tfrlem5  8116  en2sn  8718  en2snOLD  8719  mapdom1  8811  php2  8831  snnen2o  8836  frfi  8916  fodomfi  8949  ixpfi2  8974  hartogs  9160  wemapsolem  9166  card2on  9170  unwdomg  9200  r1pwss  9400  tz9.12lem3  9405  uniwf  9435  rankval3b  9442  djuun  9542  tskwe  9566  carddomi2  9586  cardsdomelir  9589  infxpenlem  9627  inffien  9677  alephord  9689  alephdom  9695  iunfictbso  9728  dfac8  9749  dfacacn  9755  dfac13  9756  dfac12lem2  9758  infmap2  9832  ackbij1b  9853  ackbij2  9857  fictb  9859  cfslb  9880  fin67  10009  fin1a2lem10  10023  fin1a2lem11  10024  dcomex  10061  ttukeylem1  10123  ttukeylem7  10129  ondomon  10177  konigthlem  10182  alephadd  10191  alephexp1  10193  alephreg  10196  pwcfsdom  10197  fpwwe2lem12  10256  gchaleph  10285  gchaleph2  10286  winainflem  10307  inttsk  10388  inar1  10389  inatsk  10392  grudomon  10431  nqerid  10547  nqpr  10628  zmin  12540  uzrdgsuci  13533  isfinite4  13929  pfxccatin12lem3  14297  limsupval2  15041  sumz  15286  fsumsers  15292  isumclim  15321  ntrivcvgfvn0  15463  ntrivcvgtail  15464  zprodn0  15501  iprodclim  15560  alzdvds  15881  bitsfzolem  15993  phicl2  16321  phibnd  16324  pclem  16391  strle1  16711  fnpr2ob  17063  psss  18086  symg2bas  18785  dprdss  19416  2ndcdisj  22353  dis2ndc  22357  hausmapdom  22397  ptcnplem  22518  fbun  22737  metrest  23422  opnreen  23728  ivthle  24353  ivthle2  24354  ovolfiniun  24398  volfiniun  24444  uniiccdif  24475  uniioovol  24476  uniioombllem4  24483  dyadmbl  24497  vitali  24510  mbflimsup  24563  cpnres  24834  dvcj  24847  dvef  24877  dvne0  24908  lhop2  24912  itgparts  24944  itgsubstlem  24945  ply1divex  25034  fta1blem  25066  dgrlem  25123  pige3ALT  25409  xrlimcnp  25851  ftalem3  25957  lgsdchr  26236  2lgslem1  26275  addsqn2reu  26322  2sqreultblem  26329  2sqreunnltblem  26332  dchrvmasumlem2  26379  pntlem3  26490  tgisline  26718  axcontlem2  27056  upgrex  27183  umgrnloop2  27237  usgriedgleord  27316  uspgredgleord  27320  nbedgusgr  27460  nb3grprlem2  27469  rusgrnumwrdl2  27674  wlkp1lem2  27762  wwlksnexthasheq  27987  wlksnwwlknvbij  27992  2pthon3v  28027  umgr2wlk  28033  rusgrnumwlkg  28061  umgrclwwlkge2  28074  clwwlkvbij  28196  0pthonv  28212  1pthon2v  28236  numclwwlkqhash  28458  chscllem4  29721  adjeq  30016  hmopidmchi  30232  xreceu  30916  tocyccntz  31130  archirngz  31162  archiabllem1b  31165  locfinreflem  31504  measvuni  31894  elmbfmvol2  31946  omsmeas  32002  sibfof  32019  eulerpartlemgvv  32055  ballotlemfc0  32171  ballotlemfcc  32172  iccllysconn  32925  cvmliftphtlem  32992  satfv1  33038  sat1el2xp  33054  ttrclss  33519  opnrebl2  34247  re1ax2lem  34313  re1ax2  34314  bj-orim2  34473  bj-peircecurry  34475  lindsdom  35508  poimir  35547  volsupnfl  35559  areacirc  35607  totbndbnd  35684  islsati  36745  hdmap14lem2a  39618  rabdiophlem1  40326  pellexlem5  40358  ttac  40561  aomclem4  40585  hbtlem5  40656  idomodle  40724  idomsubgmo  40726  rp-isfinite5  40809  iscard4  40825  mnuunid  41568  vk15.4j  41821  ax6e2nd  41851  trsspwALT2  42112  sspwtrALT  42115  sstrALT2  42128  dvmptconst  43131  dvmptidg  43133  fperdvper  43135  dvmulcncf  43141  dvdivcncf  43143  fourierdlem20  43343  fouriercn  43448  ndmaovcl  44367  fundcmpsurinjpreimafv  44533  fmtnofac2  44694  prminf2  44713  isomuspgrlem2  44958  irinitoringc  45300  pgrpgt2nabl  45375  line2x  45773  prstchom2ALT  46031  spcdvw  46056  aacllem  46176