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  1972  snssg  4736  relcnvtrg  6214  relresfld  6223  onfr  6345  foimacnv  6780  fvi  6898  isoini2  7273  ovidig  7488  f1oexbi  7858  frxp  8056  smores2  8274  tfrlem5  8299  en2sn  8963  en2prd  8969  mapdom1  9055  frfi  9169  fodomfi  9196  fodomfiOLD  9214  ixpfi2  9234  hartogs  9430  wemapsolem  9436  card2on  9440  unwdomg  9470  ttrclss  9610  r1pwss  9674  tz9.12lem3  9679  uniwf  9709  rankval3b  9716  djuun  9816  tskwe  9840  carddomi2  9860  cardsdomelir  9863  infxpenlem  9901  inffien  9951  alephord  9963  alephdom  9969  iunfictbso  10002  dfac8  10024  dfacacn  10030  dfac13  10031  dfac12lem2  10033  infmap2  10105  ackbij1b  10126  ackbij2  10130  fictb  10132  cfslb  10154  fin67  10283  fin1a2lem10  10297  fin1a2lem11  10298  dcomex  10335  ttukeylem1  10397  ttukeylem7  10403  ondomon  10451  konigthlem  10456  alephadd  10465  alephexp1  10467  alephreg  10470  pwcfsdom  10471  fpwwe2lem12  10530  gchaleph  10559  gchaleph2  10560  winainflem  10581  inttsk  10662  inar1  10663  inatsk  10666  grudomon  10705  nqerid  10821  nqpr  10902  zmin  12839  uzrdgsuci  13864  isfinite4  14266  pfxccatin12lem3  14636  limsupval2  15384  sumz  15626  fsumsers  15632  isumclim  15661  ntrivcvgfvn0  15803  ntrivcvgtail  15804  zprodn0  15843  iprodclim  15902  alzdvds  16228  bitsfzolem  16342  phicl2  16676  phibnd  16679  pclem  16747  strle1  17066  fnpr2ob  17459  psss  18483  symg2bas  19303  dprdss  19941  irinitoringc  21414  2ndcdisj  23369  dis2ndc  23373  hausmapdom  23413  ptcnplem  23534  fbun  23753  metrest  24437  opnreen  24745  ivthle  25382  ivthle2  25383  ovolfiniun  25427  volfiniun  25473  uniiccdif  25504  uniioovol  25505  uniioombllem4  25512  dyadmbl  25526  vitali  25539  mbflimsup  25592  cpnres  25864  dvcj  25879  dvef  25909  dvne0  25941  lhop2  25945  itgparts  25979  itgsubstlem  25980  ply1divex  26067  fta1blem  26101  dgrlem  26159  pige3ALT  26454  xrlimcnp  26903  ftalem3  27010  lgsdchr  27291  2lgslem1  27330  addsqn2reu  27377  2sqreultblem  27384  2sqreunnltblem  27387  dchrvmasumlem2  27434  pntlem3  27545  mulsproplem13  28065  mulsproplem14  28066  tgisline  28603  axcontlem2  28941  upgrex  29068  umgrnloop2  29122  usgriedgleord  29204  uspgredgleord  29208  nbedgusgr  29348  nb3grprlem2  29357  rusgrnumwrdl2  29563  wlkp1lem2  29649  wwlksnexthasheq  29879  wlksnwwlknvbij  29884  2pthon3v  29919  umgr2wlk  29925  rusgrnumwlkg  29953  umgrclwwlkge2  29966  clwwlkvbij  30088  0pthonv  30104  1pthon2v  30128  numclwwlkqhash  30350  chscllem4  31615  adjeq  31910  hmopidmchi  32126  xreceu  32897  tocyccntz  33108  archirngz  33153  archiabllem1b  33156  locfinreflem  33848  measvuni  34222  elmbfmvol2  34275  omsmeas  34331  sibfof  34348  eulerpartlemgvv  34384  ballotlemfc0  34501  ballotlemfcc  34502  rankval4b  35104  iccllysconn  35282  cvmliftphtlem  35349  satfv1  35395  sat1el2xp  35411  opnrebl2  36354  re1ax2lem  36420  re1ax2  36421  bj-orim2  36589  bj-peircecurry  36591  lindsdom  37653  poimir  37692  volsupnfl  37704  areacirc  37752  totbndbnd  37828  islsati  39032  hdmap14lem2a  41905  rabdiophlem1  42833  pellexlem5  42865  ttac  43068  aomclem4  43089  hbtlem5  43160  idomodle  43223  idomsubgmo  43225  nnoeomeqom  43344  omabs2  43364  rp-isfinite5  43549  iscard4  43565  mnuunid  44309  vk15.4j  44560  ax6e2nd  44590  trsspwALT2  44850  sspwtrALT  44853  sstrALT2  44866  permaxrep  45038  dvmptconst  45952  dvmptidg  45954  fperdvper  45956  dvmulcncf  45962  dvdivcncf  45964  fourierdlem20  46164  fouriercn  46269  ndmaovcl  47233  fundcmpsurinjpreimafv  47438  fmtnofac2  47599  prminf2  47618  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpgprismgr4cyclex  48137  gpg5edgnedg  48160  pgrpgt2nabl  48396  line2x  48785  prstchom2ALT  49595  spcdvw  49710  aacllem  49832