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  1702  tbwlem2  1703  re1luk3  1709  merco1lem17  1730  re1tbw1  1742  spimew  1970  relcnvtrg  6114  relresfld  6122  onfr  6225  foimacnv  6627  fvi  6735  isoini2  7086  ovidig  7286  f1oexbi  7627  frxp  7814  smores2  7985  tfrlem5  8010  mapdom1  8676  php2  8696  snnen2o  8701  frfi  8757  fodomfi  8791  ixpfi2  8816  hartogs  9002  wemapsolem  9008  card2on  9012  unwdomg  9042  r1pwss  9207  tz9.12lem3  9212  uniwf  9242  rankval3b  9249  djuun  9349  tskwe  9373  carddomi2  9393  cardsdomelir  9396  infxpenlem  9433  inffien  9483  alephord  9495  alephdom  9501  iunfictbso  9534  dfac8  9555  dfacacn  9561  dfac13  9562  dfac12lem2  9564  infmap2  9634  ackbij1b  9655  ackbij2  9659  fictb  9661  cfslb  9682  fin67  9811  fin1a2lem10  9825  fin1a2lem11  9826  dcomex  9863  ttukeylem1  9925  ttukeylem7  9931  ondomon  9979  konigthlem  9984  alephadd  9993  alephexp1  9995  alephreg  9998  pwcfsdom  9999  fpwwe2lem13  10058  gchaleph  10087  gchaleph2  10088  winainflem  10109  inttsk  10190  inar1  10191  inatsk  10194  grudomon  10233  nqerid  10349  nqpr  10430  zmin  12338  uzrdgsuci  13322  isfinite4  13717  pfxccatin12lem3  14088  limsupval2  14831  sumz  15073  fsumsers  15079  isumclim  15106  ntrivcvgfvn0  15249  ntrivcvgtail  15250  zprodn0  15287  iprodclim  15346  alzdvds  15664  bitsfzolem  15777  phicl2  16099  phibnd  16102  pclem  16169  strle1  16586  fnpr2ob  16825  psss  17818  symg2bas  18515  dprdss  19145  2ndcdisj  22058  dis2ndc  22062  hausmapdom  22102  ptcnplem  22223  fbun  22442  metrest  23128  opnreen  23433  ivthle  24051  ivthle2  24052  ovolfiniun  24096  volfiniun  24142  uniiccdif  24173  uniioovol  24174  uniioombllem4  24181  dyadmbl  24195  vitali  24208  mbflimsup  24261  cpnres  24528  dvcj  24541  dvef  24571  dvne0  24602  lhop2  24606  itgparts  24638  itgsubstlem  24639  ply1divex  24724  fta1blem  24756  dgrlem  24813  pige3ALT  25099  xrlimcnp  25540  ftalem3  25646  lgsdchr  25925  2lgslem1  25964  addsqn2reu  26011  2sqreultblem  26018  2sqreunnltblem  26021  dchrvmasumlem2  26068  pntlem3  26179  tgisline  26407  axcontlem2  26745  upgrex  26871  umgrnloop2  26925  usgriedgleord  27004  uspgredgleord  27008  nbedgusgr  27148  nb3grprlem2  27157  rusgrnumwrdl2  27362  wlkp1lem2  27450  wwlksnexthasheq  27675  wlksnwwlknvbij  27681  2pthon3v  27716  umgr2wlk  27722  rusgrnumwlkg  27750  umgrclwwlkge2  27763  clwwlkvbij  27886  0pthonv  27902  1pthon2v  27926  numclwwlkqhash  28148  chscllem4  29411  adjeq  29706  hmopidmchi  29922  xreceu  30593  tocyccntz  30781  archirngz  30813  archiabllem1b  30816  locfinreflem  31099  measvuni  31468  elmbfmvol2  31520  omsmeas  31576  sibfof  31593  eulerpartlemgvv  31629  ballotlemfc0  31745  ballotlemfcc  31746  iccllysconn  32492  cvmliftphtlem  32559  satfv1  32605  sat1el2xp  32621  opnrebl2  33664  re1ax2lem  33730  re1ax2  33731  bj-orim2  33886  bj-peircecurry  33888  lindsdom  34880  poimir  34919  volsupnfl  34931  areacirc  34981  totbndbnd  35061  islsati  36124  hdmap14lem2a  38997  rabdiophlem1  39391  pellexlem5  39423  ttac  39626  aomclem4  39650  hbtlem5  39721  idomodle  39789  idomsubgmo  39791  rp-isfinite5  39876  iscard4  39893  mnuunid  40606  vk15.4j  40855  ax6e2nd  40885  trsspwALT2  41146  sspwtrALT  41149  sstrALT2  41162  dvmptconst  42191  dvmptidg  42193  fperdvper  42195  dvmulcncf  42202  dvdivcncf  42204  fourierdlem20  42405  fouriercn  42510  ndmaovcl  43395  fundcmpsurinjpreimafv  43561  fmtnofac2  43724  prminf2  43743  isomuspgrlem2  43991  irinitoringc  44333  pgrpgt2nabl  44407  line2x  44734  spcdvw  44775  aacllem  44895