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  1978  snssg  4722  relcnvtrg  6225  relresfld  6234  onfr  6356  foimacnv  6791  fvi  6910  isoini2  7290  ovidig  7505  f1oexbi  7875  frxp  8073  smores2  8291  tfrlem5  8316  en2sn  8985  en2prd  8991  mapdom1  9077  frfi  9192  fodomfi  9219  fodomfiOLD  9237  ixpfi2  9257  hartogs  9456  wemapsolem  9462  card2on  9466  unwdomg  9496  ttrclss  9639  r1pwss  9706  tz9.12lem3  9711  uniwf  9741  rankval3b  9748  djuun  9848  tskwe  9872  carddomi2  9892  cardsdomelir  9895  infxpenlem  9933  inffien  9983  alephord  9995  alephdom  10001  iunfictbso  10034  dfac8  10056  dfacacn  10062  dfac13  10063  dfac12lem2  10065  infmap2  10137  ackbij1b  10158  ackbij2  10162  fictb  10164  cfslb  10186  fin67  10315  fin1a2lem10  10329  fin1a2lem11  10330  dcomex  10367  ttukeylem1  10429  ttukeylem7  10435  ondomon  10483  konigthlem  10489  alephadd  10498  alephexp1  10500  alephreg  10503  pwcfsdom  10504  fpwwe2lem12  10563  gchaleph  10592  gchaleph2  10593  winainflem  10614  inttsk  10695  inar1  10696  inatsk  10699  grudomon  10738  nqerid  10854  nqpr  10935  zmin  12892  uzrdgsuci  13920  isfinite4  14322  pfxccatin12lem3  14692  limsupval2  15440  sumz  15682  fsumsers  15688  isumclim  15717  ntrivcvgfvn0  15862  ntrivcvgtail  15863  zprodn0  15902  iprodclim  15961  alzdvds  16287  bitsfzolem  16401  phicl2  16736  phibnd  16739  pclem  16807  strle1  17126  fnpr2ob  17520  psss  18544  symg2bas  19366  dprdss  20004  irinitoringc  21461  2ndcdisj  23446  dis2ndc  23450  hausmapdom  23490  ptcnplem  23611  fbun  23830  metrest  24514  opnreen  24822  ivthle  25448  ivthle2  25449  ovolfiniun  25493  volfiniun  25539  uniiccdif  25570  uniioovol  25571  uniioombllem4  25578  dyadmbl  25592  vitali  25605  mbflimsup  25658  cpnres  25929  dvcj  25942  dvef  25972  dvne0  26003  lhop2  26007  itgparts  26039  itgsubstlem  26040  ply1divex  26127  fta1blem  26161  dgrlem  26219  pige3ALT  26509  xrlimcnp  26957  ftalem3  27063  lgsdchr  27343  2lgslem1  27382  addsqn2reu  27429  2sqreultblem  27436  2sqreunnltblem  27439  dchrvmasumlem2  27486  pntlem3  27597  mulsproplem13  28145  mulsproplem14  28146  tgisline  28720  axcontlem2  29059  upgrex  29186  umgrnloop2  29240  usgriedgleord  29322  uspgredgleord  29326  nbedgusgr  29466  nb3grprlem2  29475  rusgrnumwrdl2  29680  wlkp1lem2  29766  wwlksnexthasheq  29996  wlksnwwlknvbij  30001  2pthon3v  30036  umgr2wlk  30042  rusgrnumwlkg  30073  umgrclwwlkge2  30086  clwwlkvbij  30208  0pthonv  30224  1pthon2v  30248  numclwwlkqhash  30470  chscllem4  31736  adjeq  32031  hmopidmchi  32247  xreceu  33007  tocyccntz  33232  archirngz  33277  archiabllem1b  33280  locfinreflem  34031  measvuni  34405  elmbfmvol2  34458  omsmeas  34514  sibfof  34531  eulerpartlemgvv  34567  ballotlemfc0  34684  ballotlemfcc  34685  rankval4b  35288  iccllysconn  35485  cvmliftphtlem  35552  satfv1  35598  sat1el2xp  35614  opnrebl2  36556  re1ax2lem  36622  re1ax2  36623  regsfromregtco  36773  bj-orim2  36873  bj-peircecurry  36875  lindsdom  37988  poimir  38027  volsupnfl  38039  areacirc  38087  totbndbnd  38163  islsati  39493  hdmap14lem2a  42366  rabdiophlem1  43253  pellexlem5  43285  ttac  43488  aomclem4  43509  hbtlem5  43580  idomodle  43643  idomsubgmo  43645  nnoeomeqom  43764  omabs2  43784  rp-isfinite5  43968  iscard4  43984  mnuunid  44728  vk15.4j  44979  ax6e2nd  45009  trsspwALT2  45269  sspwtrALT  45272  sstrALT2  45285  permaxrep  45457  dvmptconst  46365  dvmptidg  46367  fperdvper  46369  dvmulcncf  46375  dvdivcncf  46377  fourierdlem20  46577  fouriercn  46682  ndmaovcl  47673  fundcmpsurinjpreimafv  47890  fmtnofac2  48054  prminf2  48073  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpgprismgr4cyclex  48605  gpg5edgnedg  48628  pgrpgt2nabl  48864  line2x  49252  prstchom2ALT  50061  spcdvw  50176  aacllem  50298