Theorem sylancl 409

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 408	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  411  sylanblrc  412  equveli  1732  sseqtrid  3147  ssdifin0  3444  uneqdifeqim  3448  unimax  3770  opth  4159  djussxp  4684  iss  4865  relresfld  5068  eldmrexrn  5561  f1oresrab  5585  fmptco  5586  fsn  5592  fnressn  5606  foima2  5653  foeqcnvco  5691  isoini2  5720  ofres  5996  ofco  6000  tposexg  6155  tfrlemisucaccv  6222  tfrlemibex  6226  tfri1dALT  6248  tfrcl  6261  rdgivallem  6278  frecabex  6295  frectfr  6297  frecrdg  6305  pmresg  6570  mapsn  6584  mapsncnv  6589  ixpsnf1o  6630  en1  6693  2dom  6699  enpr2d  6711  mapxpen  6742  phplem4  6749  fiintim  6817  sbthlem2  6846  elfir  6861  infglbti  6912  caseinl  6976  caseinr  6977  difinfsnlem  6984  difinfsn  6985  exmidfodomrlemim  7057  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  archnqq  7225  prarloclemlt  7301  prarloclemlo  7302  prarloclemcalc  7310  recexprlemm  7432  recexprlemex  7445  caucvgprlemm  7476  caucvgprprlemmu  7503  suplocexprlem2b  7522  suplocexprlemmu  7526  suplocexprlemlub  7532  1idsr  7576  recexgt0sr  7581  archsr  7590  caucvgsrlemoffval  7604  caucvgsrlemofff  7605  caucvgsrlemoffres  7608  caucvgsr  7610  ltpsrprg  7611  suplocsrlem  7616  pitonnlem2  7655  pitonn  7656  pitoregt0  7657  pitore  7658  recnnre  7659  axrnegex  7687  nntopi  7702  msqge0  8378  mulge0  8381  recexaplem2  8413  recexap  8414  recgt0  8608  recreclt  8658  nn1m1nn  8738  nn1suc  8739  nnle1eq1  8744  nn1gt1  8754  nnsub  8759  addltmul  8956  nn0le0eq0  9005  elnn0nn  9019  elnnz  9064  elznn0  9069  zlem1lt  9110  zltlem1  9111  elz2  9122  nn0n0n1ge2b  9130  nn0lt2  9132  nn0le2is012  9133  eluzaddi  9352  eluzsubi  9353  uzp1  9359  peano2uzr  9380  nn01to3  9409  qreccl  9434  ltpnf  9567  xaddass2  9653  fz01en  9833  fzpreddisj  9851  fzsuc2  9859  fseq1p1m1  9874  fseq1m1p1  9875  elfzp1b  9877  fzoss2  9949  fzval3  9981  fzosplitsnm1  9986  fzosplitprm1  10011  flhalf  10075  modqmulnn  10115  modqmuladdnn0  10141  frec2uzrand  10178  frecuzrdg0  10186  frecuzrdg0t  10195  frecfzennn  10199  frecfzen2  10200  uzennn  10209  seqeq1  10221  seq3m1  10241  monoord2  10250  ser3mono  10251  ser0f  10288  exp3vallem  10294  expm1t  10321  expeq0  10324  expubnd  10350  binom3  10409  facndiv  10485  facavg  10492  bcn0  10501  bcnp1n  10505  bcm1k  10506  bcp1nk  10508  bcval5  10509  bcn2  10510  bcp1m1  10511  bcpasc  10512  bcn2m1  10515  hashsng  10544  hashun  10551  hashfz  10567  hashfzo  10568  seq3coll  10585  shftfval  10593  2shfti  10603  resqrexlemf1  10780  abs00ap  10834  sqabs  10854  ltabs  10859  caubnd2  10889  max0addsup  10991  rexico  10993  mulcn2  11081  climaddc1  11098  climmulc2  11100  climsubc1  11101  climsubc2  11102  iserex  11108  climlec2  11110  iser3shft  11115  climcvg1nlem  11118  serf0  11121  sumrbdc  11148  fsumm1  11185  fsump1  11189  fsum00  11231  telfsumo  11235  fsumparts  11239  hashiun  11247  binomlem  11252  binom1dif  11256  bcxmas  11258  isumsplit  11260  isum1p  11261  arisum  11267  arisum2  11268  trireciplem  11269  explecnv  11274  geolim  11280  georeclim  11282  mertenslem2  11305  mertensabs  11306  prodf1f  11312  prodrbdclem2  11342  efcllemp  11364  ef0lem  11366  efgt0  11390  eftlub  11396  efsep  11397  effsumlt  11398  tanval3ap  11421  efi4p  11424  resin4p  11425  recos4p  11426  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  cos01gt0  11469  absefib  11477  efieq1re  11478  eirraplem  11483  dvdsdc  11501  dvdscmulr  11522  dvdslelemd  11541  odd2np1lem  11569  odd2np1  11570  flodddiv4  11631  gcdsupex  11646  gcdsupcl  11647  gcd1  11675  nn0seqcvgd  11722  algcvg  11729  algcvgblem  11730  eucalg  11740  prmind2  11801  qden1elz  11883  dfphi2  11896  phiprm  11899  phimullem  11901  oddennn  11905  xpct  11909  ennnfonelemj0  11914  ennnfonelemen  11934  ctinfomlemom  11940  restid  12131  restuni2  12346  cnrest2r  12406  lmfss  12413  lmres  12417  lmtopcnp  12419  ispsmet  12492  isxmet2d  12517  ismet2  12523  blfvalps  12554  blex  12556  xblss2  12574  reopnap  12707  divcnap  12724  climcncf  12740  cncfmpt2fcntop  12754  limcdifap  12800  cnplimcim  12805  cnlimcim  12809  cnlimc  12810  cnlimci  12811  dvbss  12823  dvcnp2cntop  12832  dvcn  12833  dvaddxxbr  12834  dvmulxxbr  12835  dvexp  12844  dveflem  12855  sinperlem  12889  sin2kpi  12892  cos2kpi  12893  sin2pim  12894  cos2pim  12895  cosq14gt0  12913  coseq0q4123  12915  tangtx  12919  abssinper  12927  sinkpi  12928  coskpi  12929  cosq34lt1  12931  pwle2  13193  nninfsellemdc  13206  sbthom  13221