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 ⊢ (𝜓 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  spimew  2003  snssg  4740  relcnvtrgOLD  6269  relresfldOLD  6279  onfr  6402  foimacnv  6842  fvi  6961  isoini2  7347  ovidig  7562  f1oexbi  7940  frxp  8140  smores2  8365  tfrlem5  8390  en2sn  9072  en2prd  9078  mapdom1  9164  frfi  9279  fodomfi  9307  ixpfi2  9342  hartogs  9541  wemapsolem  9547  card2on  9551  unwdomg  9581  ttrclss  9724  r1pwss  9794  tz9.12lem3  9799  uniwf  9831  rankval3b  9839  rankval4b  9883  spcdvw  9973  djuun  10010  tskwe  10034  carddomi2  10054  cardsdomelir  10057  infxpenlem  10095  inffien  10145  alephord  10157  alephdom  10163  iunfictbso  10196  dfac8  10217  dfacacn  10223  dfac13  10224  dfac12lem2  10226  infmap2  10298  ackbij1b  10319  ackbij2  10323  fictb  10325  cfslb  10347  fin67  10476  fin1a2lem10  10490  fin1a2lem11  10491  dcomex  10528  ttukeylem1  10590  ttukeylem7  10596  ondomon  10650  konigthlem  10656  alephadd  10665  alephexp1  10667  alephreg  10670  pwcfsdom  10671  fpwwe2lem12  10730  gchaleph  10759  gchaleph2  10760  winainflem  10781  inttsk  10862  inar1  10863  inatsk  10866  grudomon  10905  nqerid  11021  nqpr  11102  zmin  13074  uzrdgsuci  14106  isfinite4  14509  pfxccatin12lem3  14885  limsupval2  15652  sumz  15893  fsumsers  15899  isumclim  15928  ntrivcvgfvn0  16073  ntrivcvgtail  16074  zprodn0  16111  iprodclim  16170  alzdvds  16495  bitsfzolem  16609  phicl2  16950  phibnd  16953  pclem  17021  strle1  17341  fnpr2ob  17735  psss  18759  symg2bas  19612  dprdss  20250  irinitoringc  21790  lindsdom  22161  2ndcdisj  23780  dis2ndc  23784  hausmapdom  23824  ptcnplem  23945  fbun  24164  metrest  24848  opnreen  25156  ivthle  25782  ivthle2  25783  ovolfiniun  25827  volfiniun  25873  uniiccdif  25904  uniioovol  25905  uniioombllem4  25912  dyadmbl  25926  vitali  25939  mbflimsup  25992  cpnres  26262  dvcj  26275  dvef  26305  dvne0  26336  lhop2  26340  itgparts  26372  itgsubstlem  26373  ply1divex  26460  fta1blem  26494  dgrlem  26553  pige3ALT  26853  xrlimcnp  27301  ftalem3  27407  lgsdchr  27687  2lgslem1  27726  addsqn2reu  27773  2sqreultblem  27780  2sqreunnltblem  27783  dchrvmasumlem2  27830  pntlem3  27941  mulsproplem13  28519  mulsproplem14  28520  tgisline  29100  axcontlem2  29548  upgrex  29675  umgrnloop2  29729  usgriedgleord  29814  uspgredgleord  29818  nbedgusgr  29958  nb3grprlem2  29967  rusgrnumwrdl2  30172  wlkp1lem2  30258  wwlksnexthasheq  30497  wlksnwwlknvbij  30502  2pthon3v  30537  umgr2wlk  30543  rusgrnumwlkg  30574  umgrclwwlkge2  30587  clwwlkvbij  30709  0pthonv  30725  1pthon2v  30759  numclwwlkqhash  30981  chscllem4  32247  adjeq  32542  hmopidmchi  32758  xreceu  33534  tocyccntz  33751  archirngz  33796  archiabllem1b  33799  locfinreflem  34518  measvuni  34893  elmbfmvol2  34945  omsmeas  35001  sibfof  35018  eulerpartlemgvv  35054  ballotlemfc0  35171  ballotlemfcc  35172  onprcf1acwevdlem2  35965  iccllysconn  36101  cvmliftphtlem  36168  satfv1  36214  sat1el2xp  36230  opnrebl2  37201  re1ax2lem  37267  re1ax2  37268  regsfromregtco  37418  bj-orim2  37517  bj-peircecurry  37519  poimir  38664  volsupnfl  38676  areacirc  38724  totbndbnd  38816  islsati  40144  hdmap14lem2a  43017  rabdiophlem1  43901  pellexlem5  43933  ttac  44136  aomclem4  44152  hbtlem5  44223  idomodle  44286  idomsubgmo  44288  nnoeomeqom  44407  omabs2  44427  rp-isfinite5  44611  iscard4  44627  mnuunid  45354  vk15.4j  45604  ax6e2nd  45634  trsspwALT2  45894  sspwtrALT  45897  sstrALT2  45910  permaxrep  46089  dvmptconst  47018  dvmptidg  47020  fperdvper  47022  dvmulcncf  47028  dvdivcncf  47030  fourierdlem20  47230  fouriercn  47335  ndmaovcl  48366  fundcmpsurinjpreimafv  48583  fmtnofac2  48747  prminf2  48766  gpg5nbgrvtx03starlem1  49259  gpg5nbgrvtx03starlem2  49260  gpg5nbgrvtx03starlem3  49261  gpg5nbgrvtx13starlem1  49262  gpg5nbgrvtx13starlem2  49263  gpg5nbgrvtx13starlem3  49264  gpgprismgr4cyclex  49298  gpg5edgnedg  49321  pgrpgt2nabl  49571  prstchom2ALT  50795  aacllem  51107