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  1701  tbwlem2  1702  re1luk3  1708  merco1lem17  1729  re1tbw1  1741  spimew  1968  snssg  4787  relcnvtrg  6287  relresfld  6297  onfr  6424  foimacnv  6865  fvi  6984  isoini2  7358  ovidig  7574  f1oexbi  7950  frxp  8149  smores2  8392  tfrlem5  8418  en2sn  9079  en2prd  9086  mapdom1  9180  php2OLD  9257  snnen2oOLD  9261  frfi  9318  fodomfi  9347  fodomfiOLD  9367  ixpfi2  9387  hartogs  9581  wemapsolem  9587  card2on  9591  unwdomg  9621  ttrclss  9757  r1pwss  9821  tz9.12lem3  9826  uniwf  9856  rankval3b  9863  djuun  9963  tskwe  9987  carddomi2  10007  cardsdomelir  10010  infxpenlem  10050  inffien  10100  alephord  10112  alephdom  10118  iunfictbso  10151  dfac8  10173  dfacacn  10179  dfac13  10180  dfac12lem2  10182  infmap2  10254  ackbij1b  10275  ackbij2  10279  fictb  10281  cfslb  10303  fin67  10432  fin1a2lem10  10446  fin1a2lem11  10447  dcomex  10484  ttukeylem1  10546  ttukeylem7  10552  ondomon  10600  konigthlem  10605  alephadd  10614  alephexp1  10616  alephreg  10619  pwcfsdom  10620  fpwwe2lem12  10679  gchaleph  10708  gchaleph2  10709  winainflem  10730  inttsk  10811  inar1  10812  inatsk  10815  grudomon  10854  nqerid  10970  nqpr  11051  zmin  12983  uzrdgsuci  13997  isfinite4  14397  pfxccatin12lem3  14766  limsupval2  15512  sumz  15754  fsumsers  15760  isumclim  15789  ntrivcvgfvn0  15931  ntrivcvgtail  15932  zprodn0  15971  iprodclim  16030  alzdvds  16353  bitsfzolem  16467  phicl2  16801  phibnd  16804  pclem  16871  strle1  17191  fnpr2ob  17604  psss  18637  symg2bas  19424  dprdss  20063  irinitoringc  21507  2ndcdisj  23479  dis2ndc  23483  hausmapdom  23523  ptcnplem  23644  fbun  23863  metrest  24552  opnreen  24866  ivthle  25504  ivthle2  25505  ovolfiniun  25549  volfiniun  25595  uniiccdif  25626  uniioovol  25627  uniioombllem4  25634  dyadmbl  25648  vitali  25661  mbflimsup  25714  cpnres  25987  dvcj  26002  dvef  26032  dvne0  26064  lhop2  26068  itgparts  26102  itgsubstlem  26103  ply1divex  26190  fta1blem  26224  dgrlem  26282  pige3ALT  26576  xrlimcnp  27025  ftalem3  27132  lgsdchr  27413  2lgslem1  27452  addsqn2reu  27499  2sqreultblem  27506  2sqreunnltblem  27509  dchrvmasumlem2  27556  pntlem3  27667  mulsproplem13  28168  mulsproplem14  28169  tgisline  28649  axcontlem2  28994  upgrex  29123  umgrnloop2  29177  usgriedgleord  29259  uspgredgleord  29263  nbedgusgr  29403  nb3grprlem2  29412  rusgrnumwrdl2  29618  wlkp1lem2  29706  wwlksnexthasheq  29932  wlksnwwlknvbij  29937  2pthon3v  29972  umgr2wlk  29978  rusgrnumwlkg  30006  umgrclwwlkge2  30019  clwwlkvbij  30141  0pthonv  30157  1pthon2v  30181  numclwwlkqhash  30403  chscllem4  31668  adjeq  31963  hmopidmchi  32179  xreceu  32888  tocyccntz  33146  archirngz  33178  archiabllem1b  33181  locfinreflem  33800  measvuni  34194  elmbfmvol2  34248  omsmeas  34304  sibfof  34321  eulerpartlemgvv  34357  ballotlemfc0  34473  ballotlemfcc  34474  iccllysconn  35234  cvmliftphtlem  35301  satfv1  35347  sat1el2xp  35363  opnrebl2  36303  re1ax2lem  36369  re1ax2  36370  bj-orim2  36538  bj-peircecurry  36540  lindsdom  37600  poimir  37639  volsupnfl  37651  areacirc  37699  totbndbnd  37775  islsati  38975  hdmap14lem2a  41849  rabdiophlem1  42788  pellexlem5  42820  ttac  43024  aomclem4  43045  hbtlem5  43116  idomodle  43179  idomsubgmo  43181  nnoeomeqom  43301  omabs2  43321  rp-isfinite5  43506  iscard4  43522  mnuunid  44272  vk15.4j  44525  ax6e2nd  44555  trsspwALT2  44816  sspwtrALT  44819  sstrALT2  44832  dvmptconst  45870  dvmptidg  45872  fperdvper  45874  dvmulcncf  45880  dvdivcncf  45882  fourierdlem20  46082  fouriercn  46187  ndmaovcl  47152  fundcmpsurinjpreimafv  47332  fmtnofac2  47493  prminf2  47512  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  pgrpgt2nabl  48210  line2x  48603  prstchom2ALT  48879  spcdvw  48909  aacllem  49031