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  1707  tbwlem2  1708  re1luk3  1714  merco1lem17  1735  re1tbw1  1747  spimew  1975  snssg  4780  relcnvtrg  6254  relresfld  6264  onfr  6392  foimacnv  6837  fvi  6953  isoini2  7320  ovidig  7533  f1oexbi  7901  frxp  8094  smores2  8336  tfrlem5  8362  en2sn  9024  en2snOLD  9025  en2prd  9031  mapdom1  9125  php2OLD  9206  snnen2oOLD  9210  frfi  9271  fodomfi  9308  ixpfi2  9333  hartogs  9521  wemapsolem  9527  card2on  9531  unwdomg  9561  ttrclss  9697  r1pwss  9761  tz9.12lem3  9766  uniwf  9796  rankval3b  9803  djuun  9903  tskwe  9927  carddomi2  9947  cardsdomelir  9950  infxpenlem  9990  inffien  10040  alephord  10052  alephdom  10058  iunfictbso  10091  dfac8  10112  dfacacn  10118  dfac13  10119  dfac12lem2  10121  infmap2  10195  ackbij1b  10216  ackbij2  10220  fictb  10222  cfslb  10243  fin67  10372  fin1a2lem10  10386  fin1a2lem11  10387  dcomex  10424  ttukeylem1  10486  ttukeylem7  10492  ondomon  10540  konigthlem  10545  alephadd  10554  alephexp1  10556  alephreg  10559  pwcfsdom  10560  fpwwe2lem12  10619  gchaleph  10648  gchaleph2  10649  winainflem  10670  inttsk  10751  inar1  10752  inatsk  10755  grudomon  10794  nqerid  10910  nqpr  10991  zmin  12910  uzrdgsuci  13907  isfinite4  14304  pfxccatin12lem3  14664  limsupval2  15406  sumz  15650  fsumsers  15656  isumclim  15685  ntrivcvgfvn0  15827  ntrivcvgtail  15828  zprodn0  15865  iprodclim  15924  alzdvds  16245  bitsfzolem  16357  phicl2  16683  phibnd  16686  pclem  16753  strle1  17073  fnpr2ob  17486  psss  18515  symg2bas  19224  dprdss  19858  2ndcdisj  22889  dis2ndc  22893  hausmapdom  22933  ptcnplem  23054  fbun  23273  metrest  23962  opnreen  24276  ivthle  24902  ivthle2  24903  ovolfiniun  24947  volfiniun  24993  uniiccdif  25024  uniioovol  25025  uniioombllem4  25032  dyadmbl  25046  vitali  25059  mbflimsup  25112  cpnres  25383  dvcj  25396  dvef  25426  dvne0  25457  lhop2  25461  itgparts  25493  itgsubstlem  25494  ply1divex  25583  fta1blem  25615  dgrlem  25672  pige3ALT  25958  xrlimcnp  26400  ftalem3  26506  lgsdchr  26785  2lgslem1  26824  addsqn2reu  26871  2sqreultblem  26878  2sqreunnltblem  26881  dchrvmasumlem2  26928  pntlem3  27039  mulsproplem13  27497  mulsproplem14  27498  tgisline  27743  axcontlem2  28088  upgrex  28217  umgrnloop2  28271  usgriedgleord  28350  uspgredgleord  28354  nbedgusgr  28494  nb3grprlem2  28503  rusgrnumwrdl2  28708  wlkp1lem2  28796  wwlksnexthasheq  29022  wlksnwwlknvbij  29027  2pthon3v  29062  umgr2wlk  29068  rusgrnumwlkg  29096  umgrclwwlkge2  29109  clwwlkvbij  29231  0pthonv  29247  1pthon2v  29271  numclwwlkqhash  29493  chscllem4  30756  adjeq  31051  hmopidmchi  31267  xreceu  31959  tocyccntz  32174  archirngz  32206  archiabllem1b  32209  locfinreflem  32651  measvuni  33043  elmbfmvol2  33097  omsmeas  33153  sibfof  33170  eulerpartlemgvv  33206  ballotlemfc0  33322  ballotlemfcc  33323  iccllysconn  34072  cvmliftphtlem  34139  satfv1  34185  sat1el2xp  34201  opnrebl2  35010  re1ax2lem  35076  re1ax2  35077  bj-orim2  35236  bj-peircecurry  35238  lindsdom  36286  poimir  36325  volsupnfl  36337  areacirc  36385  totbndbnd  36462  islsati  37669  hdmap14lem2a  40543  rabdiophlem1  41310  pellexlem5  41342  ttac  41546  aomclem4  41570  hbtlem5  41641  idomodle  41709  idomsubgmo  41711  nnoeomeqom  41833  omabs2  41853  rp-isfinite5  42039  iscard4  42055  mnuunid  42807  vk15.4j  43060  ax6e2nd  43090  trsspwALT2  43351  sspwtrALT  43354  sstrALT2  43367  dvmptconst  44404  dvmptidg  44406  fperdvper  44408  dvmulcncf  44414  dvdivcncf  44416  fourierdlem20  44616  fouriercn  44721  ndmaovcl  45683  fundcmpsurinjpreimafv  45848  fmtnofac2  46009  prminf2  46028  isomuspgrlem2  46273  irinitoringc  46615  pgrpgt2nabl  46690  line2x  47088  prstchom2ALT  47347  spcdvw  47372  aacllem  47496