Theorem sylancl 410

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancl.1	|- ( ph -> ps )
sylancl.2	|- ch
sylancl.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylancl	|- ( ph -> th )

Proof of Theorem sylancl

Step	Hyp	Ref	Expression
1		sylancl.1	. 2 |- ( ph -> ps )
2		sylancl.2	. . 3 |- ch
3	2	a1i 9	. 2 |- ( ph -> ch )
4		sylancl.3	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 3, 4	syl2anc 409	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  sylanblc  412  sylanblrc  413  equveli  1739  sseqtrid  3178  ssdifin0  3475  uneqdifeqim  3479  unimax  3806  opth  4197  djussxp  4730  iss  4911  relresfld  5114  eldmrexrn  5607  f1oresrab  5631  fmptco  5632  fsn  5638  fnressn  5652  foima2  5699  foeqcnvco  5737  isoini2  5766  ofres  6043  ofco  6047  tposexg  6202  tfrlemisucaccv  6269  tfrlemibex  6273  tfri1dALT  6295  tfrcl  6308  rdgivallem  6325  frecabex  6342  frectfr  6344  frecrdg  6352  pmresg  6618  mapsn  6632  mapsncnv  6637  ixpsnf1o  6678  en1  6741  2dom  6747  enpr2d  6759  mapxpen  6790  phplem4  6797  fiintim  6870  sbthlem2  6899  elfir  6914  infglbti  6965  caseinl  7029  caseinr  7030  difinfsnlem  7037  difinfsn  7038  nninfisollemne  7068  exmidfodomrlemim  7130  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  archnqq  7331  prarloclemlt  7407  prarloclemlo  7408  prarloclemcalc  7416  recexprlemm  7538  recexprlemex  7551  caucvgprlemm  7582  caucvgprprlemmu  7609  suplocexprlem2b  7628  suplocexprlemmu  7632  suplocexprlemlub  7638  1idsr  7682  recexgt0sr  7687  archsr  7696  caucvgsrlemoffval  7710  caucvgsrlemofff  7711  caucvgsrlemoffres  7714  caucvgsr  7716  ltpsrprg  7717  suplocsrlem  7722  pitonnlem2  7761  pitonn  7762  pitoregt0  7763  pitore  7764  recnnre  7765  axrnegex  7793  nntopi  7808  msqge0  8485  mulge0  8488  recexaplem2  8520  recexap  8521  recgt0  8715  recreclt  8765  nn1m1nn  8845  nn1suc  8846  nnle1eq1  8851  nn1gt1  8861  nnsub  8866  addltmul  9063  nn0le0eq0  9112  elnn0nn  9126  elnnz  9171  elznn0  9176  zlem1lt  9217  zltlem1  9218  elz2  9229  nn0n0n1ge2b  9237  nn0lt2  9239  nn0le2is012  9240  eluzaddi  9459  eluzsubi  9460  uzp1  9466  peano2uzr  9490  nn01to3  9519  qreccl  9544  ltpnf  9680  xaddass2  9767  iccen  9903  fz01en  9948  fzpreddisj  9966  fzsuc2  9974  fseq1p1m1  9989  fseq1m1p1  9990  elfzp1b  9992  fzoss2  10064  fzval3  10096  fzosplitsnm1  10101  fzosplitprm1  10126  flhalf  10194  modqmulnn  10234  modqmuladdnn0  10260  frec2uzrand  10297  frecuzrdg0  10305  frecuzrdg0t  10314  frecfzennn  10318  frecfzen2  10319  uzennn  10328  seqeq1  10340  seq3m1  10360  monoord2  10369  ser3mono  10370  ser0f  10407  exp3vallem  10413  expm1t  10440  expeq0  10443  expubnd  10469  binom3  10528  facndiv  10606  facavg  10613  bcn0  10622  bcnp1n  10626  bcm1k  10627  bcp1nk  10629  bcval5  10630  bcn2  10631  bcp1m1  10632  bcpasc  10633  bcn2m1  10636  hashsng  10665  hashun  10672  hashfz  10688  hashfzo  10689  seq3coll  10706  shftfval  10714  2shfti  10724  resqrexlemf1  10901  abs00ap  10955  sqabs  10975  ltabs  10980  caubnd2  11010  max0addsup  11112  rexico  11114  mulcn2  11202  climaddc1  11219  climmulc2  11221  climsubc1  11222  climsubc2  11223  iserex  11229  climlec2  11231  iser3shft  11236  climcvg1nlem  11239  serf0  11242  sumrbdc  11269  fsumm1  11306  fsump1  11310  fsum00  11352  telfsumo  11356  fsumparts  11360  hashiun  11368  binomlem  11373  binom1dif  11377  bcxmas  11379  isumsplit  11381  isum1p  11382  arisum  11388  arisum2  11389  trireciplem  11390  explecnv  11395  geolim  11401  georeclim  11403  mertenslem2  11426  mertensabs  11427  prodf1f  11433  prodrbdclem2  11463  efcllemp  11548  ef0lem  11550  efgt0  11574  eftlub  11580  efsep  11581  effsumlt  11582  tanval3ap  11604  efi4p  11607  resin4p  11608  recos4p  11609  ef01bndlem  11646  sin01bnd  11647  cos01bnd  11648  sin01gt0  11651  cos01gt0  11652  absefib  11660  efieq1re  11661  eirraplem  11666  dvdsdc  11687  dvdscmulr  11708  dvdslelemd  11727  odd2np1lem  11755  odd2np1  11756  flodddiv4  11817  gcdsupex  11832  gcdsupcl  11833  gcd1  11862  nn0seqcvgd  11909  algcvg  11916  algcvgblem  11917  eucalg  11927  prmind2  11988  qden1elz  12070  dfphi2  12083  phiprm  12086  phimullem  12088  prmdiv  12098  prmdiveq  12099  oddennn  12104  xpct  12108  ennnfonelemj0  12113  ennnfonelemen  12133  ctinfomlemom  12139  omctfn  12155  restid  12333  restuni2  12548  cnrest2r  12608  lmfss  12615  lmres  12619  lmtopcnp  12621  ispsmet  12694  isxmet2d  12719  ismet2  12725  blfvalps  12756  blex  12758  xblss2  12776  reopnap  12909  divcnap  12926  climcncf  12942  cncfmpt2fcntop  12956  limcdifap  13002  cnplimcim  13007  cnlimcim  13011  cnlimc  13012  cnlimci  13013  dvbss  13025  dvcnp2cntop  13034  dvcn  13035  dvaddxxbr  13036  dvmulxxbr  13037  dvexp  13046  dveflem  13058  reeff1olem  13063  sinperlem  13100  sin2kpi  13103  cos2kpi  13104  sin2pim  13105  cos2pim  13106  cosq14gt0  13124  coseq0q4123  13126  tangtx  13130  abssinper  13138  sinkpi  13139  coskpi  13140  cosq34lt1  13142  logrpap0b  13168  logdivlti  13173  rpcxpsqrtth  13221  rpabscxpbnd  13230  binom4  13267  pwle2  13541  pw1nct  13546  nninfsellemdc  13553  sbthom  13568  trirec0  13586  apdifflemr  13589  reap0  13600  nconstwlpolem  13606