Theorem mpsyl 69

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 66	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  2001  snssg  4750  relcnvtrg  6270  relresfld  6279  onfr  6402  foimacnv  6840  fvi  6959  isoini2  7339  ovidig  7554  f1oexbi  7926  frxp  8123  smores2  8342  tfrlem5  8367  en2sn  9039  en2prd  9045  mapdom1  9131  frfi  9246  fodomfi  9273  ixpfi2  9308  hartogs  9507  wemapsolem  9513  card2on  9517  unwdomg  9547  ttrclss  9690  r1pwss  9757  tz9.12lem3  9762  uniwf  9792  rankval3b  9799  djuun  9913  tskwe  9937  carddomi2  9957  cardsdomelir  9960  infxpenlem  9998  inffien  10048  alephord  10060  alephdom  10066  iunfictbso  10099  dfac8  10120  dfacacn  10126  dfac13  10127  dfac12lem2  10129  infmap2  10201  ackbij1b  10222  ackbij2  10226  fictb  10228  cfslb  10251  fin67  10380  fin1a2lem10  10394  fin1a2lem11  10395  dcomex  10432  ttukeylem1  10494  ttukeylem7  10500  ondomon  10548  konigthlem  10554  alephadd  10563  alephexp1  10565  alephreg  10568  pwcfsdom  10569  fpwwe2lem12  10628  gchaleph  10657  gchaleph2  10658  winainflem  10679  inttsk  10760  inar1  10761  inatsk  10764  grudomon  10803  nqerid  10919  nqpr  11000  zmin  12969  uzrdgsuci  13998  isfinite4  14400  pfxccatin12lem3  14771  limsupval2  15533  sumz  15775  fsumsers  15781  isumclim  15810  ntrivcvgfvn0  15955  ntrivcvgtail  15956  zprodn0  15995  iprodclim  16054  alzdvds  16379  bitsfzolem  16493  phicl2  16828  phibnd  16831  pclem  16899  strle1  17219  fnpr2ob  17613  psss  18637  symg2bas  19464  dprdss  20102  irinitoringc  21610  2ndcdisj  23594  dis2ndc  23598  hausmapdom  23638  ptcnplem  23759  fbun  23978  metrest  24662  opnreen  24970  ivthle  25596  ivthle2  25597  ovolfiniun  25641  volfiniun  25687  uniiccdif  25718  uniioovol  25719  uniioombllem4  25726  dyadmbl  25740  vitali  25753  mbflimsup  25806  cpnres  26077  dvcj  26090  dvef  26120  dvne0  26151  lhop2  26155  itgparts  26187  itgsubstlem  26188  ply1divex  26275  fta1blem  26309  dgrlem  26367  pige3ALT  26666  xrlimcnp  27114  ftalem3  27220  lgsdchr  27500  2lgslem1  27539  addsqn2reu  27586  2sqreultblem  27593  2sqreunnltblem  27596  dchrvmasumlem2  27643  pntlem3  27754  mulsproplem13  28302  mulsproplem14  28303  tgisline  28881  axcontlem2  29296  upgrex  29423  umgrnloop2  29477  usgriedgleord  29559  uspgredgleord  29563  nbedgusgr  29703  nb3grprlem2  29712  rusgrnumwrdl2  29917  wlkp1lem2  30003  wwlksnexthasheq  30233  wlksnwwlknvbij  30238  2pthon3v  30273  umgr2wlk  30279  rusgrnumwlkg  30310  umgrclwwlkge2  30323  clwwlkvbij  30445  0pthonv  30461  1pthon2v  30485  numclwwlkqhash  30707  chscllem4  31973  adjeq  32268  hmopidmchi  32484  xreceu  33222  tocyccntz  33445  archirngz  33490  archiabllem1b  33493  locfinreflem  34211  measvuni  34585  elmbfmvol2  34638  omsmeas  34694  sibfof  34711  eulerpartlemgvv  34747  ballotlemfc0  34864  ballotlemfcc  34865  rankval4b  35474  iccllysconn  35723  cvmliftphtlem  35790  satfv1  35836  sat1el2xp  35852  opnrebl2  36813  re1ax2lem  36879  re1ax2  36880  regsfromregtco  37030  bj-orim2  37129  bj-peircecurry  37131  lindsdom  38246  poimir  38285  volsupnfl  38297  areacirc  38345  totbndbnd  38421  islsati  39749  hdmap14lem2a  42622  rabdiophlem1  43511  pellexlem5  43543  ttac  43746  aomclem4  43767  hbtlem5  43838  idomodle  43901  idomsubgmo  43903  nnoeomeqom  44022  omabs2  44042  rp-isfinite5  44226  iscard4  44242  mnuunid  44970  vk15.4j  45220  ax6e2nd  45250  trsspwALT2  45510  sspwtrALT  45513  sstrALT2  45526  permaxrep  45698  dvmptconst  46612  dvmptidg  46614  fperdvper  46616  dvmulcncf  46622  dvdivcncf  46624  fourierdlem20  46824  fouriercn  46929  ndmaovcl  47923  fundcmpsurinjpreimafv  48140  fmtnofac2  48304  prminf2  48323  gpg5nbgrvtx03starlem1  48816  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx13starlem1  48819  gpg5nbgrvtx13starlem2  48820  gpg5nbgrvtx13starlem3  48821  gpgprismgr4cyclex  48855  gpg5edgnedg  48878  pgrpgt2nabl  49129  line2x  49517  prstchom2ALT  50325  spcdvw  50440  aacllem  50584