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  1703  tbwlem2  1704  re1luk3  1710  merco1lem17  1731  re1tbw1  1743  spimew  1971  snssg  4808  relcnvtrg  6297  relresfld  6307  onfr  6434  foimacnv  6879  fvi  6998  isoini2  7375  ovidig  7592  f1oexbi  7968  frxp  8167  smores2  8410  tfrlem5  8436  en2sn  9106  en2snOLD  9107  en2prd  9114  mapdom1  9208  php2OLD  9286  snnen2oOLD  9290  frfi  9349  fodomfi  9378  fodomfiOLD  9398  ixpfi2  9420  hartogs  9613  wemapsolem  9619  card2on  9623  unwdomg  9653  ttrclss  9789  r1pwss  9853  tz9.12lem3  9858  uniwf  9888  rankval3b  9895  djuun  9995  tskwe  10019  carddomi2  10039  cardsdomelir  10042  infxpenlem  10082  inffien  10132  alephord  10144  alephdom  10150  iunfictbso  10183  dfac8  10205  dfacacn  10211  dfac13  10212  dfac12lem2  10214  infmap2  10286  ackbij1b  10307  ackbij2  10311  fictb  10313  cfslb  10335  fin67  10464  fin1a2lem10  10478  fin1a2lem11  10479  dcomex  10516  ttukeylem1  10578  ttukeylem7  10584  ondomon  10632  konigthlem  10637  alephadd  10646  alephexp1  10648  alephreg  10651  pwcfsdom  10652  fpwwe2lem12  10711  gchaleph  10740  gchaleph2  10741  winainflem  10762  inttsk  10843  inar1  10844  inatsk  10847  grudomon  10886  nqerid  11002  nqpr  11083  zmin  13009  uzrdgsuci  14011  isfinite4  14411  pfxccatin12lem3  14780  limsupval2  15526  sumz  15770  fsumsers  15776  isumclim  15805  ntrivcvgfvn0  15947  ntrivcvgtail  15948  zprodn0  15987  iprodclim  16046  alzdvds  16368  bitsfzolem  16480  phicl2  16815  phibnd  16818  pclem  16885  strle1  17205  fnpr2ob  17618  psss  18650  symg2bas  19434  dprdss  20073  irinitoringc  21513  2ndcdisj  23485  dis2ndc  23489  hausmapdom  23529  ptcnplem  23650  fbun  23869  metrest  24558  opnreen  24872  ivthle  25510  ivthle2  25511  ovolfiniun  25555  volfiniun  25601  uniiccdif  25632  uniioovol  25633  uniioombllem4  25640  dyadmbl  25654  vitali  25667  mbflimsup  25720  cpnres  25993  dvcj  26008  dvef  26038  dvne0  26070  lhop2  26074  itgparts  26108  itgsubstlem  26109  ply1divex  26196  fta1blem  26230  dgrlem  26288  pige3ALT  26580  xrlimcnp  27029  ftalem3  27136  lgsdchr  27417  2lgslem1  27456  addsqn2reu  27503  2sqreultblem  27510  2sqreunnltblem  27513  dchrvmasumlem2  27560  pntlem3  27671  mulsproplem13  28172  mulsproplem14  28173  tgisline  28653  axcontlem2  28998  upgrex  29127  umgrnloop2  29181  usgriedgleord  29263  uspgredgleord  29267  nbedgusgr  29407  nb3grprlem2  29416  rusgrnumwrdl2  29622  wlkp1lem2  29710  wwlksnexthasheq  29936  wlksnwwlknvbij  29941  2pthon3v  29976  umgr2wlk  29982  rusgrnumwlkg  30010  umgrclwwlkge2  30023  clwwlkvbij  30145  0pthonv  30161  1pthon2v  30185  numclwwlkqhash  30407  chscllem4  31672  adjeq  31967  hmopidmchi  32183  xreceu  32886  tocyccntz  33137  archirngz  33169  archiabllem1b  33172  locfinreflem  33786  measvuni  34178  elmbfmvol2  34232  omsmeas  34288  sibfof  34305  eulerpartlemgvv  34341  ballotlemfc0  34457  ballotlemfcc  34458  iccllysconn  35218  cvmliftphtlem  35285  satfv1  35331  sat1el2xp  35347  opnrebl2  36287  re1ax2lem  36353  re1ax2  36354  bj-orim2  36522  bj-peircecurry  36524  lindsdom  37574  poimir  37613  volsupnfl  37625  areacirc  37673  totbndbnd  37749  islsati  38950  hdmap14lem2a  41824  rabdiophlem1  42757  pellexlem5  42789  ttac  42993  aomclem4  43014  hbtlem5  43085  idomodle  43152  idomsubgmo  43154  nnoeomeqom  43274  omabs2  43294  rp-isfinite5  43479  iscard4  43495  mnuunid  44246  vk15.4j  44499  ax6e2nd  44529  trsspwALT2  44790  sspwtrALT  44793  sstrALT2  44806  dvmptconst  45836  dvmptidg  45838  fperdvper  45840  dvmulcncf  45846  dvdivcncf  45848  fourierdlem20  46048  fouriercn  46153  ndmaovcl  47118  fundcmpsurinjpreimafv  47282  fmtnofac2  47443  prminf2  47462  pgrpgt2nabl  48091  line2x  48488  prstchom2ALT  48746  spcdvw  48771  aacllem  48895