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  1972  snssg  4735  relcnvtrg  6219  relresfld  6228  onfr  6350  foimacnv  6785  fvi  6904  isoini2  7279  ovidig  7494  f1oexbi  7864  frxp  8062  smores2  8280  tfrlem5  8305  en2sn  8970  en2prd  8976  mapdom1  9062  frfi  9176  fodomfi  9203  fodomfiOLD  9221  ixpfi2  9241  hartogs  9437  wemapsolem  9443  card2on  9447  unwdomg  9477  ttrclss  9617  r1pwss  9684  tz9.12lem3  9689  uniwf  9719  rankval3b  9726  djuun  9826  tskwe  9850  carddomi2  9870  cardsdomelir  9873  infxpenlem  9911  inffien  9961  alephord  9973  alephdom  9979  iunfictbso  10012  dfac8  10034  dfacacn  10040  dfac13  10041  dfac12lem2  10043  infmap2  10115  ackbij1b  10136  ackbij2  10140  fictb  10142  cfslb  10164  fin67  10293  fin1a2lem10  10307  fin1a2lem11  10308  dcomex  10345  ttukeylem1  10407  ttukeylem7  10413  ondomon  10461  konigthlem  10466  alephadd  10475  alephexp1  10477  alephreg  10480  pwcfsdom  10481  fpwwe2lem12  10540  gchaleph  10569  gchaleph2  10570  winainflem  10591  inttsk  10672  inar1  10673  inatsk  10676  grudomon  10715  nqerid  10831  nqpr  10912  zmin  12844  uzrdgsuci  13869  isfinite4  14271  pfxccatin12lem3  14641  limsupval2  15389  sumz  15631  fsumsers  15637  isumclim  15666  ntrivcvgfvn0  15808  ntrivcvgtail  15809  zprodn0  15848  iprodclim  15907  alzdvds  16233  bitsfzolem  16347  phicl2  16681  phibnd  16684  pclem  16752  strle1  17071  fnpr2ob  17464  psss  18488  symg2bas  19307  dprdss  19945  irinitoringc  21418  2ndcdisj  23372  dis2ndc  23376  hausmapdom  23416  ptcnplem  23537  fbun  23756  metrest  24440  opnreen  24748  ivthle  25385  ivthle2  25386  ovolfiniun  25430  volfiniun  25476  uniiccdif  25507  uniioovol  25508  uniioombllem4  25515  dyadmbl  25529  vitali  25542  mbflimsup  25595  cpnres  25867  dvcj  25882  dvef  25912  dvne0  25944  lhop2  25948  itgparts  25982  itgsubstlem  25983  ply1divex  26070  fta1blem  26104  dgrlem  26162  pige3ALT  26457  xrlimcnp  26906  ftalem3  27013  lgsdchr  27294  2lgslem1  27333  addsqn2reu  27380  2sqreultblem  27387  2sqreunnltblem  27390  dchrvmasumlem2  27437  pntlem3  27548  mulsproplem13  28068  mulsproplem14  28069  tgisline  28606  axcontlem2  28945  upgrex  29072  umgrnloop2  29126  usgriedgleord  29208  uspgredgleord  29212  nbedgusgr  29352  nb3grprlem2  29361  rusgrnumwrdl2  29567  wlkp1lem2  29653  wwlksnexthasheq  29883  wlksnwwlknvbij  29888  2pthon3v  29923  umgr2wlk  29929  rusgrnumwlkg  29960  umgrclwwlkge2  29973  clwwlkvbij  30095  0pthonv  30111  1pthon2v  30135  numclwwlkqhash  30357  chscllem4  31622  adjeq  31917  hmopidmchi  32133  xreceu  32909  tocyccntz  33120  archirngz  33165  archiabllem1b  33168  locfinreflem  33874  measvuni  34248  elmbfmvol2  34301  omsmeas  34357  sibfof  34374  eulerpartlemgvv  34410  ballotlemfc0  34527  ballotlemfcc  34528  rankval4b  35132  iccllysconn  35315  cvmliftphtlem  35382  satfv1  35428  sat1el2xp  35444  opnrebl2  36386  re1ax2lem  36452  re1ax2  36453  bj-orim2  36621  bj-peircecurry  36623  lindsdom  37674  poimir  37713  volsupnfl  37725  areacirc  37773  totbndbnd  37849  islsati  39113  hdmap14lem2a  41986  rabdiophlem1  42918  pellexlem5  42950  ttac  43153  aomclem4  43174  hbtlem5  43245  idomodle  43308  idomsubgmo  43310  nnoeomeqom  43429  omabs2  43449  rp-isfinite5  43634  iscard4  43650  mnuunid  44394  vk15.4j  44645  ax6e2nd  44675  trsspwALT2  44935  sspwtrALT  44938  sstrALT2  44951  permaxrep  45123  dvmptconst  46037  dvmptidg  46039  fperdvper  46041  dvmulcncf  46047  dvdivcncf  46049  fourierdlem20  46249  fouriercn  46354  ndmaovcl  47327  fundcmpsurinjpreimafv  47532  fmtnofac2  47693  prminf2  47712  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpgprismgr4cyclex  48231  gpg5edgnedg  48254  pgrpgt2nabl  48490  line2x  48879  prstchom2ALT  49689  spcdvw  49804  aacllem  49926