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:  spimew  1971  snssg  4783  relcnvtrg  6286  relresfld  6296  onfr  6423  foimacnv  6865  fvi  6985  isoini2  7359  ovidig  7575  f1oexbi  7950  frxp  8151  smores2  8394  tfrlem5  8420  en2sn  9081  en2prd  9088  mapdom1  9182  php2OLD  9260  snnen2oOLD  9264  frfi  9321  fodomfi  9350  fodomfiOLD  9370  ixpfi2  9390  hartogs  9584  wemapsolem  9590  card2on  9594  unwdomg  9624  ttrclss  9760  r1pwss  9824  tz9.12lem3  9829  uniwf  9859  rankval3b  9866  djuun  9966  tskwe  9990  carddomi2  10010  cardsdomelir  10013  infxpenlem  10053  inffien  10103  alephord  10115  alephdom  10121  iunfictbso  10154  dfac8  10176  dfacacn  10182  dfac13  10183  dfac12lem2  10185  infmap2  10257  ackbij1b  10278  ackbij2  10282  fictb  10284  cfslb  10306  fin67  10435  fin1a2lem10  10449  fin1a2lem11  10450  dcomex  10487  ttukeylem1  10549  ttukeylem7  10555  ondomon  10603  konigthlem  10608  alephadd  10617  alephexp1  10619  alephreg  10622  pwcfsdom  10623  fpwwe2lem12  10682  gchaleph  10711  gchaleph2  10712  winainflem  10733  inttsk  10814  inar1  10815  inatsk  10818  grudomon  10857  nqerid  10973  nqpr  11054  zmin  12986  uzrdgsuci  14001  isfinite4  14401  pfxccatin12lem3  14770  limsupval2  15516  sumz  15758  fsumsers  15764  isumclim  15793  ntrivcvgfvn0  15935  ntrivcvgtail  15936  zprodn0  15975  iprodclim  16034  alzdvds  16357  bitsfzolem  16471  phicl2  16805  phibnd  16808  pclem  16876  strle1  17195  fnpr2ob  17603  psss  18625  symg2bas  19410  dprdss  20049  irinitoringc  21490  2ndcdisj  23464  dis2ndc  23468  hausmapdom  23508  ptcnplem  23629  fbun  23848  metrest  24537  opnreen  24853  ivthle  25491  ivthle2  25492  ovolfiniun  25536  volfiniun  25582  uniiccdif  25613  uniioovol  25614  uniioombllem4  25621  dyadmbl  25635  vitali  25648  mbflimsup  25701  cpnres  25973  dvcj  25988  dvef  26018  dvne0  26050  lhop2  26054  itgparts  26088  itgsubstlem  26089  ply1divex  26176  fta1blem  26210  dgrlem  26268  pige3ALT  26562  xrlimcnp  27011  ftalem3  27118  lgsdchr  27399  2lgslem1  27438  addsqn2reu  27485  2sqreultblem  27492  2sqreunnltblem  27495  dchrvmasumlem2  27542  pntlem3  27653  mulsproplem13  28154  mulsproplem14  28155  tgisline  28635  axcontlem2  28980  upgrex  29109  umgrnloop2  29163  usgriedgleord  29245  uspgredgleord  29249  nbedgusgr  29389  nb3grprlem2  29398  rusgrnumwrdl2  29604  wlkp1lem2  29692  wwlksnexthasheq  29923  wlksnwwlknvbij  29928  2pthon3v  29963  umgr2wlk  29969  rusgrnumwlkg  29997  umgrclwwlkge2  30010  clwwlkvbij  30132  0pthonv  30148  1pthon2v  30172  numclwwlkqhash  30394  chscllem4  31659  adjeq  31954  hmopidmchi  32170  xreceu  32904  tocyccntz  33164  archirngz  33196  archiabllem1b  33199  locfinreflem  33839  measvuni  34215  elmbfmvol2  34269  omsmeas  34325  sibfof  34342  eulerpartlemgvv  34378  ballotlemfc0  34495  ballotlemfcc  34496  iccllysconn  35255  cvmliftphtlem  35322  satfv1  35368  sat1el2xp  35384  opnrebl2  36322  re1ax2lem  36388  re1ax2  36389  bj-orim2  36557  bj-peircecurry  36559  lindsdom  37621  poimir  37660  volsupnfl  37672  areacirc  37720  totbndbnd  37796  islsati  38995  hdmap14lem2a  41869  rabdiophlem1  42812  pellexlem5  42844  ttac  43048  aomclem4  43069  hbtlem5  43140  idomodle  43203  idomsubgmo  43205  nnoeomeqom  43325  omabs2  43345  rp-isfinite5  43530  iscard4  43546  mnuunid  44296  vk15.4j  44548  ax6e2nd  44578  trsspwALT2  44839  sspwtrALT  44842  sstrALT2  44855  dvmptconst  45930  dvmptidg  45932  fperdvper  45934  dvmulcncf  45940  dvdivcncf  45942  fourierdlem20  46142  fouriercn  46247  ndmaovcl  47215  fundcmpsurinjpreimafv  47395  fmtnofac2  47556  prminf2  47575  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  pgrpgt2nabl  48282  line2x  48675  prstchom2ALT  49168  spcdvw  49198  aacllem  49320