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  1806  tbwlem2  1807  re1luk3  1813  merco1lem17  1834  re1tbw1  1846  relcnvtr  5897  relresfld  5904  onfr  6003  foimacnv  6396  fvi  6503  isoini2  6845  ovidig  7039  f1oexbi  7379  frxp  7552  smores2  7718  tfrlem5  7743  mapdom1  8395  php2  8415  snnen2o  8419  frfi  8475  fodomfi  8509  ixpfi2  8534  hartogs  8719  wemapsolem  8725  card2on  8729  unwdomg  8759  r1pwss  8925  tz9.12lem3  8930  uniwf  8960  rankval3b  8967  djuun  9066  tskwe  9090  carddomi2  9110  cardsdomelir  9113  infxpenlem  9150  inffien  9200  alephord  9212  alephdom  9218  iunfictbso  9251  dfac8  9273  dfacacn  9279  dfac13  9280  dfac12lem2  9282  infmap2  9356  ackbij1b  9377  ackbij2  9381  fictb  9383  cfslb  9404  fin67  9533  fin1a2lem10  9547  fin1a2lem11  9548  dcomex  9585  ttukeylem1  9647  ttukeylem7  9653  ondomon  9701  konigthlem  9706  alephadd  9715  alephexp1  9717  alephreg  9720  pwcfsdom  9721  fpwwe2lem13  9780  gchaleph  9809  gchaleph2  9810  winainflem  9831  inttsk  9912  inar1  9913  inatsk  9916  grudomon  9955  nqerid  10071  nqpr  10152  zmin  12068  uzrdgsuci  13055  isfinite4  13444  swrdccatin12lem3  13831  limsupval2  14589  sumz  14831  fsumsers  14837  isumclim  14864  ntrivcvgfvn0  15005  ntrivcvgtail  15006  zprodn0  15043  iprodclim  15102  alzdvds  15420  bitsfzolem  15530  phicl2  15845  phibnd  15848  pclem  15915  strle1  16333  psss  17568  symg2bas  18169  dprdss  18783  2ndcdisj  21631  dis2ndc  21635  hausmapdom  21675  ptcnplem  21796  fbun  22015  metrest  22700  opnreen  23005  ivthle  23623  ivthle2  23624  ovolfiniun  23668  volfiniun  23714  uniiccdif  23745  uniioovol  23746  uniioombllem4  23753  dyadmbl  23767  vitali  23780  mbflimsup  23833  cpnres  24100  dvcj  24113  dvef  24143  dvne0  24174  lhop2  24178  itgparts  24210  itgsubstlem  24211  ply1divex  24296  fta1blem  24328  dgrlem  24385  pige3  24670  xrlimcnp  25109  ftalem3  25215  lgsdchr  25494  2lgslem1  25533  dchrvmasumlem2  25601  pntlem3  25712  tgisline  25940  axcontlem2  26265  upgrex  26391  umgrnloop2  26446  usgriedgleord  26525  uspgredgleord  26530  nbedgusgr  26671  nb3grprlem2  26680  rusgrnumwrdl2  26885  wlkp1lem2  26976  wlknwwlksnbij2OLD  27194  wlkwwlkbij2OLD  27201  wwlksnexthasheq  27224  wwlksnexthasheqOLD  27225  wlksnwwlknvbij  27231  wlksnwwlknvbijOLD  27232  2pthon3v  27273  umgr2wlk  27279  rusgrnumwlkg  27308  umgrclwwlkge2  27321  clwwlkvbij  27489  clwwlkvbijOLD  27490  0pthonv  27506  1pthon2v  27530  numclwwlk1lem2OLDOLD  27759  numclwwlkqhash  27779  chscllem4  29055  adjeq  29350  hmopidmchi  29566  xreceu  30176  archirngz  30289  archiabllem1b  30292  locfinreflem  30453  measvuni  30823  elmbfmvol2  30875  omsmeas  30931  sibfof  30948  eulerpartlemgvv  30984  ballotlemfc0  31101  ballotlemfcc  31102  iccllysconn  31779  cvmliftphtlem  31846  opnrebl2  32855  re1ax2lem  32921  re1ax2  32922  bj-orim2  33073  bj-currypeirce  33075  bj-peircecurry  33076  lindsdom  33948  poimir  33987  volsupnfl  33999  areacirc  34049  totbndbnd  34131  islsati  35070  hdmap14lem2a  37943  rabdiophlem1  38210  pellexlem5  38242  ttac  38447  aomclem4  38471  hbtlem5  38542  idomodle  38618  idomsubgmo  38620  rp-isfinite5  38705  vk15.4j  39573  ax6e2nd  39603  eel0001  39774  trsspwALT2  39874  sspwtrALT  39877  sstrALT2  39890  dvmptconst  40925  dvmptidg  40927  fperdvper  40929  dvmulcncf  40936  dvdivcncf  40938  fourierdlem20  41139  fouriercn  41244  ndmaovcl  42106  fmtnofac2  42312  prminf2  42331  isomuspgrlem2  42552  irinitoringc  42917  pgrpgt2nabl  42995  line2x  43307  spcdvw  43322  aacllem  43444