Theorem mpsyl 66

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 63	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  1621  tbwlem2  1622  re1luk3  1628  merco1lem17  1649  re1tbw1  1661  relcnvtr  5572  relresfld  5579  onfr  5680  foimacnv  6067  fvi  6165  isoini2  6489  ovidig  6676  f1oexbi  7009  frxp  7174  smores2  7338  tfrlem5  7363  mapdom1  8010  php2  8030  snnen2o  8034  frfi  8090  fodomfi  8124  ixpfi2  8147  hartogs  8332  wemapsolem  8338  card2on  8342  unwdomg  8372  r1pwss  8530  tz9.12lem3  8535  uniwf  8565  rankval3b  8572  tskwe  8659  carddomi2  8679  cardsdomelir  8682  infxpenlem  8719  inffien  8769  alephord  8781  alephdom  8787  iunfictbso  8820  dfac8  8840  dfacacn  8846  dfac13  8847  dfac12lem2  8849  infmap2  8923  ackbij1b  8944  ackbij2  8948  fictb  8950  cfslb  8971  fin67  9100  fin1a2lem10  9114  fin1a2lem11  9115  dcomex  9152  ttukeylem1  9214  ttukeylem7  9220  ondomon  9264  konigthlem  9269  alephadd  9278  alephexp1  9280  alephreg  9283  pwcfsdom  9284  fpwwe2lem13  9343  gchaleph  9372  gchaleph2  9373  winainflem  9394  inttsk  9475  inar1  9476  inatsk  9479  grudomon  9518  nqerid  9634  nqpr  9715  zmin  11660  uzrdgsuci  12621  isfinite4  13014  swrdccatin12lem3  13341  limsupval2  14059  caucvgb  14258  sumz  14300  fsumsers  14306  isumclim  14330  isumnn0nn  14413  climcndslem1  14420  climcndslem2  14421  ntrivcvgfvn0  14470  ntrivcvgtail  14471  zprodn0  14508  iprodclim  14568  alzdvds  14880  bitsfzolem  14994  phicl2  15311  phibnd  15314  pclem  15381  strle1  15800  psss  17037  symg2bas  17641  dprdss  18251  2ndcdisj  21069  dis2ndc  21073  hausmapdom  21113  ptcnplem  21234  fbun  21454  metrest  22139  opnreen  22442  bndth  22565  cmetcaulem  22894  ivthle  23032  ivthle2  23033  ovolfiniun  23076  volfiniun  23122  uniiccdif  23152  uniioovol  23153  uniioombllem4  23160  dyadmbl  23174  vitali  23188  mbfdm  23201  mbflimsup  23239  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  cpnres  23506  dvcj  23519  dvef  23547  dvne0  23578  lhop2  23582  itgparts  23614  itgsubstlem  23615  ply1divex  23700  fta1blem  23732  dgrlem  23789  pige3  24073  xrlimcnp  24495  lgambdd  24563  ftalem3  24601  lgsdchr  24880  2lgslem1  24919  dchrvmasumlem2  24987  pntlem3  25098  tgisline  25322  axcontlem2  25645  upgrex  25759  umgrnloop2  25817  umgraex  25852  2trllemE  26083  0pthonv  26111  1pthon2v  26123  2pthon3v  26134  usg2wlk  26145  usg2wlkon  26146  wlknwwlknbij2  26242  wlkiswwlkbij2  26249  wwlkexthasheq  26262  wlknwwlknvbij  26268  clwwlkgt0  26299  clwwlkbij  26327  clwwlkvbij  26329  rusgrasn  26472  rusgranumwlklem4  26479  rusgranumwwlkg  26486  numclwlk1lem2  26624  numclwwlk1  26625  numclwwlkqhash  26627  chscllem4  27883  adjeq  28178  hmopidmchi  28394  xreceu  28961  archirngz  29074  archiabllem1b  29077  locfinreflem  29235  measvuni  29604  elmbfmvol2  29656  omsmeas  29712  sibfof  29729  eulerpartlemgvv  29765  ballotlemfc0  29881  ballotlemfcc  29882  iccllyscon  30486  cvmliftphtlem  30553  opnrebl2  31486  re1ax2lem  31552  re1ax2  31553  bj-orim2  31711  bj-currypeirce  31714  bj-peircecurry  31715  lindsdom  32573  poimir  32612  volsupnfl  32624  areacirc  32675  totbndbnd  32758  islsati  33299  hdmap14lem2a  36177  rabdiophlem1  36383  pellexlem5  36415  ttac  36621  aomclem4  36645  hbtlem5  36717  idomodle  36793  idomsubgmo  36795  rp-isfinite5  36882  vk15.4j  37755  ax6e2nd  37795  eel0001  37966  trsspwALT2  38068  sspwtrALT  38071  sstrALT2  38092  dvmptconst  38803  dvmptidg  38805  fperdvper  38808  dvmulcncf  38815  dvdivcncf  38817  fourierdlem20  39020  fouriercn  39125  ndmaovcl  39932  fmtnofac2  40019  prminf2  40038  usgredgleord  40455  uspgredgaleord  40459  nbedgusgr  40600  rusgrnumwrdl2  40786  1wlkp1lem2  40883  wlknwwlksnbij2  41089  wlkwwlkbij2  41096  wwlksnexthasheq  41109  wlksnwwlknvbij  41114  2pthon3v-av  41150  umgr2wlk  41156  rusgrnumwlkg  41180  umgrclwwlksge2  41219  clwwlksbij  41227  clwwlksvbij  41229  0pthonv-av  41297  1pthon2v-av  41320  av-numclwlk1lem2  41527  av-numclwwlk1  41528  av-numclwwlkqhash  41530  irinitoringc  41861  pgrpgt2nabl  41941  aacllem  42356