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:  spimew  1981  snssg  4732  relcnvtrg  6239  relresfld  6248  onfr  6370  foimacnv  6809  fvi  6928  isoini2  7308  ovidig  7523  f1oexbi  7894  frxp  8090  smores2  8309  tfrlem5  8334  en2sn  9007  en2prd  9013  mapdom1  9099  frfi  9214  fodomfi  9241  fodomfiOLD  9259  ixpfi2  9279  hartogs  9478  wemapsolem  9484  card2on  9488  unwdomg  9518  ttrclss  9661  r1pwss  9728  tz9.12lem3  9733  uniwf  9763  rankval3b  9770  djuun  9870  tskwe  9894  carddomi2  9914  cardsdomelir  9917  infxpenlem  9955  inffien  10005  alephord  10017  alephdom  10023  iunfictbso  10056  dfac8  10078  dfacacn  10084  dfac13  10085  dfac12lem2  10087  infmap2  10159  ackbij1b  10180  ackbij2  10184  fictb  10186  cfslb  10209  fin67  10338  fin1a2lem10  10352  fin1a2lem11  10353  dcomex  10390  ttukeylem1  10452  ttukeylem7  10458  ondomon  10506  konigthlem  10512  alephadd  10521  alephexp1  10523  alephreg  10526  pwcfsdom  10527  fpwwe2lem12  10586  gchaleph  10615  gchaleph2  10616  winainflem  10637  inttsk  10718  inar1  10719  inatsk  10722  grudomon  10761  nqerid  10877  nqpr  10958  zmin  12931  uzrdgsuci  13959  isfinite4  14361  pfxccatin12lem3  14731  limsupval2  15479  sumz  15721  fsumsers  15727  isumclim  15756  ntrivcvgfvn0  15901  ntrivcvgtail  15902  zprodn0  15941  iprodclim  16000  alzdvds  16326  bitsfzolem  16440  phicl2  16775  phibnd  16778  pclem  16846  strle1  17166  fnpr2ob  17560  psss  18584  symg2bas  19405  dprdss  20043  irinitoringc  21500  2ndcdisj  23485  dis2ndc  23489  hausmapdom  23529  ptcnplem  23650  fbun  23869  metrest  24553  opnreen  24861  ivthle  25487  ivthle2  25488  ovolfiniun  25532  volfiniun  25578  uniiccdif  25609  uniioovol  25610  uniioombllem4  25617  dyadmbl  25631  vitali  25644  mbflimsup  25697  cpnres  25968  dvcj  25981  dvef  26011  dvne0  26042  lhop2  26046  itgparts  26078  itgsubstlem  26079  ply1divex  26166  fta1blem  26200  dgrlem  26258  pige3ALT  26551  xrlimcnp  26999  ftalem3  27105  lgsdchr  27385  2lgslem1  27424  addsqn2reu  27471  2sqreultblem  27478  2sqreunnltblem  27481  dchrvmasumlem2  27528  pntlem3  27639  mulsproplem13  28187  mulsproplem14  28188  tgisline  28762  axcontlem2  29101  upgrex  29228  umgrnloop2  29282  usgriedgleord  29364  uspgredgleord  29368  nbedgusgr  29508  nb3grprlem2  29517  rusgrnumwrdl2  29722  wlkp1lem2  29808  wwlksnexthasheq  30038  wlksnwwlknvbij  30043  2pthon3v  30078  umgr2wlk  30084  rusgrnumwlkg  30115  umgrclwwlkge2  30128  clwwlkvbij  30250  0pthonv  30266  1pthon2v  30290  numclwwlkqhash  30512  chscllem4  31778  adjeq  32073  hmopidmchi  32289  xreceu  33049  tocyccntz  33274  archirngz  33319  archiabllem1b  33322  locfinreflem  34081  measvuni  34455  elmbfmvol2  34508  omsmeas  34564  sibfof  34581  eulerpartlemgvv  34617  ballotlemfc0  34734  ballotlemfcc  34735  rankval4b  35341  iccllysconn  35538  cvmliftphtlem  35605  satfv1  35651  sat1el2xp  35667  opnrebl2  36619  re1ax2lem  36685  re1ax2  36686  regsfromregtco  36836  bj-orim2  36936  bj-peircecurry  36938  lindsdom  38051  poimir  38090  volsupnfl  38102  areacirc  38150  totbndbnd  38226  islsati  39556  hdmap14lem2a  42429  rabdiophlem1  43316  pellexlem5  43348  ttac  43551  aomclem4  43572  hbtlem5  43643  idomodle  43706  idomsubgmo  43708  nnoeomeqom  43827  omabs2  43847  rp-isfinite5  44031  iscard4  44047  mnuunid  44791  vk15.4j  45042  ax6e2nd  45072  trsspwALT2  45332  sspwtrALT  45335  sstrALT2  45348  permaxrep  45520  dvmptconst  46427  dvmptidg  46429  fperdvper  46431  dvmulcncf  46437  dvdivcncf  46439  fourierdlem20  46639  fouriercn  46744  ndmaovcl  47735  fundcmpsurinjpreimafv  47952  fmtnofac2  48116  prminf2  48135  gpg5nbgrvtx03starlem1  48628  gpg5nbgrvtx03starlem2  48629  gpg5nbgrvtx03starlem3  48630  gpg5nbgrvtx13starlem1  48631  gpg5nbgrvtx13starlem2  48632  gpg5nbgrvtx13starlem3  48633  gpgprismgr4cyclex  48667  gpg5edgnedg  48690  pgrpgt2nabl  48926  line2x  49314  prstchom2ALT  50123  spcdvw  50238  aacllem  50360