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  2006  snssg  4744  relcnvtrgOLD  6288  relresfldOLD  6298  onfr  6423  foimacnv  6867  fvi  6987  isoini2  7373  ovidig  7589  f1oexbi  7967  frxp  8168  smores2  8393  tfrlem5  8418  en2sn  9100  en2prd  9106  mapdom1  9192  frfi  9307  fodomfi  9335  ixpfi2  9370  hartogs  9568  wemapsolem  9574  card2on  9578  unwdomg  9608  ttrclss  9751  r1pwss  9821  tz9.12lem3  9826  uniwf  9858  rankval3b  9866  rankval4b  9910  spcdvw  10000  djuun  10037  tskwe  10061  carddomi2  10081  cardsdomelir  10084  infxpenlem  10122  inffien  10172  alephord  10184  alephdom  10190  iunfictbso  10223  dfac8  10244  dfacacn  10250  dfac13  10251  dfac12lem2  10253  infmap2  10325  ackbij1b  10346  ackbij2  10350  fictb  10352  cfslb  10374  fin67  10503  fin1a2lem10  10517  fin1a2lem11  10518  dcomex  10555  ttukeylem1  10617  ttukeylem7  10623  ondomon  10677  konigthlem  10683  alephadd  10692  alephexp1  10694  alephreg  10697  pwcfsdom  10698  fpwwe2lem12  10757  gchaleph  10786  gchaleph2  10787  winainflem  10808  inttsk  10889  inar1  10890  inatsk  10893  grudomon  10932  nqerid  11048  nqpr  11129  zmin  13101  uzrdgsuci  14133  isfinite4  14536  pfxccatin12lem3  14912  limsupval2  15679  sumz  15920  fsumsers  15926  isumclim  15955  ntrivcvgfvn0  16100  ntrivcvgtail  16101  zprodn0  16138  iprodclim  16197  alzdvds  16522  bitsfzolem  16636  phicl2  16977  phibnd  16980  pclem  17048  strle1  17368  fnpr2ob  17762  psss  18786  symg2bas  19640  dprdss  20278  irinitoringc  21818  lindsdom  22189  2ndcdisj  23808  dis2ndc  23812  hausmapdom  23852  ptcnplem  23973  fbun  24192  metrest  24876  opnreen  25184  ivthle  25810  ivthle2  25811  ovolfiniun  25855  volfiniun  25901  uniiccdif  25932  uniioovol  25933  uniioombllem4  25940  dyadmbl  25954  vitali  25967  mbflimsup  26020  cpnres  26290  dvcj  26303  dvef  26333  dvne0  26364  lhop2  26368  itgparts  26400  itgsubstlem  26401  ply1divex  26488  fta1blem  26522  dgrlem  26581  pige3ALT  26881  xrlimcnp  27329  ftalem3  27435  lgsdchr  27715  2lgslem1  27754  addsqn2reu  27801  2sqreultblem  27808  2sqreunnltblem  27811  dchrvmasumlem2  27858  pntlem3  27969  mulsproplem13  28547  mulsproplem14  28548  tgisline  29128  axcontlem2  29576  upgrex  29703  umgrnloop2  29757  usgriedgleord  29842  uspgredgleord  29846  nbedgusgr  29986  nb3grprlem2  29995  rusgrnumwrdl2  30200  wlkp1lem2  30286  wwlksnexthasheq  30525  wlksnwwlknvbij  30530  2pthon3v  30565  umgr2wlk  30571  rusgrnumwlkg  30602  umgrclwwlkge2  30615  clwwlkvbij  30737  0pthonv  30753  1pthon2v  30787  numclwwlkqhash  31009  chscllem4  32275  adjeq  32570  hmopidmchi  32786  xreceu  33561  tocyccntz  33781  archirngz  33826  archiabllem1b  33829  locfinreflem  34555  measvuni  34930  elmbfmvol2  34982  omsmeas  35038  sibfof  35055  eulerpartlemgvv  35091  ballotlemfc0  35208  ballotlemfcc  35209  onprcf1acwevdlem2  36059  iccllysconn  36195  cvmliftphtlem  36262  satfv1  36308  sat1el2xp  36324  opnrebl2  37300  re1ax2lem  37366  re1ax2  37367  regsfromregtco  37517  bj-orim2  37616  bj-peircecurry  37618  poimir  38776  volsupnfl  38788  areacirc  38836  totbndbnd  38926  islsati  40254  hdmap14lem2a  43127  rabdiophlem1  44012  pellexlem5  44044  ttac  44247  aomclem4  44263  hbtlem5  44333  idomodle  44396  idomsubgmo  44398  nnoeomeqom  44517  omabs2  44537  rp-isfinite5  44721  iscard4  44737  mnuunid  45464  vk15.4j  45713  ax6e2nd  45743  trsspwALT2  46003  sspwtrALT  46006  sstrALT2  46019  permaxrep  46202  dvmptconst  47140  dvmptidg  47142  fperdvper  47144  dvmulcncf  47150  dvdivcncf  47152  fourierdlem20  47352  fouriercn  47457  ndmaovcl  48488  fundcmpsurinjpreimafv  48705  fmtnofac2  48869  prminf2  48888  gpg5nbgrvtx03starlem1  49381  gpg5nbgrvtx03starlem2  49382  gpg5nbgrvtx03starlem3  49383  gpg5nbgrvtx13starlem1  49384  gpg5nbgrvtx13starlem2  49385  gpg5nbgrvtx13starlem3  49386  gpgprismgr4cyclex  49420  gpg5edgnedg  49443  pgrpgt2nabl  49693  prstchom2ALT  50917  aacllem  51251