Theorem sylancl 405

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 404	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sylanblc  407  sylanblrc  408  equveli  1696  syl5sseq  3089  ssdifin0  3383  uneqdifeqim  3387  unimax  3709  opth  4088  djussxp  4612  iss  4791  relresfld  4994  eldmrexrn  5479  f1oresrab  5502  fmptco  5503  fsn  5508  fnressn  5522  foima2  5569  foeqcnvco  5607  isoini2  5636  ofres  5907  ofco  5911  tposexg  6061  tfrlemisucaccv  6128  tfrlemibex  6132  tfri1dALT  6154  tfrcl  6167  rdgivallem  6184  frecabex  6201  frectfr  6203  frecrdg  6211  pmresg  6473  mapsn  6487  mapsncnv  6492  ixpsnf1o  6533  en1  6596  2dom  6602  mapxpen  6644  phplem4  6651  fiintim  6719  sbthlem2  6747  infglbti  6800  caseinl  6862  exmidfodomrlemim  6924  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  archnqq  7073  prarloclemlt  7149  prarloclemlo  7150  prarloclemcalc  7158  recexprlemm  7280  recexprlemex  7293  caucvgprlemm  7324  caucvgprprlemmu  7351  1idsr  7411  recexgt0sr  7416  archsr  7424  caucvgsrlemoffval  7438  caucvgsrlemofff  7439  caucvgsrlemoffres  7442  caucvgsr  7444  pitonnlem2  7481  pitonn  7482  pitoregt0  7483  pitore  7484  recnnre  7485  axrnegex  7511  nntopi  7526  msqge0  8190  mulge0  8193  recexaplem2  8218  recexap  8219  recgt0  8408  recreclt  8458  nn1m1nn  8538  nn1suc  8539  nnle1eq1  8544  nn1gt1  8554  nnsub  8559  addltmul  8750  nn0le0eq0  8799  elnn0nn  8813  elnnz  8858  elznn0  8863  zlem1lt  8904  zltlem1  8905  elz2  8916  nn0n0n1ge2b  8924  nn0lt2  8926  nn0le2is012  8927  eluzaddi  9144  eluzsubi  9145  uzp1  9151  peano2uzr  9172  nn01to3  9201  qreccl  9226  ltpnf  9350  xaddass2  9436  fz01en  9616  fzpreddisj  9634  fzsuc2  9642  fseq1p1m1  9657  fseq1m1p1  9658  elfzp1b  9660  fzoss2  9732  fzval3  9764  fzosplitsnm1  9769  fzosplitprm1  9794  flhalf  9858  modqmulnn  9898  modqmuladdnn0  9924  frec2uzrand  9961  frecuzrdg0  9969  frecuzrdg0t  9978  frecfzennn  9982  frecfzen2  9983  seqeq1  10003  seq3m1  10018  monoord2  10027  ser3mono  10028  ser0f  10065  exp3vallem  10071  expm1t  10098  expeq0  10101  expubnd  10127  binom3  10186  facndiv  10262  facavg  10269  bcn0  10278  bcnp1n  10282  bcm1k  10283  bcp1nk  10285  bcval5  10286  bcn2  10287  bcp1m1  10288  bcpasc  10289  bcn2m1  10292  hashsng  10321  hashun  10328  hashfz  10344  hashfzo  10345  seq3coll  10362  shftfval  10370  2shfti  10380  resqrexlemf1  10556  abs00ap  10610  abs00  10612  sqabs  10630  ltabs  10635  caubnd2  10665  max0addsup  10767  rexico  10769  mulcn2  10855  climaddc1  10872  climmulc2  10874  climsubc1  10875  climsubc2  10876  iserex  10882  climlec2  10884  iser3shft  10889  climcvg1nlem  10892  serf0  10895  sumrbdc  10921  fsumm1  10959  fsump1  10963  fsum00  11005  telfsumo  11009  fsumparts  11013  hashiun  11021  binomlem  11026  binom1dif  11030  bcxmas  11032  isumsplit  11034  isum1p  11035  arisum  11041  arisum2  11042  trireciplem  11043  explecnv  11048  geolim  11054  georeclim  11056  mertenslem2  11079  mertensabs  11080  efcllemp  11097  ef0lem  11099  efgt0  11123  eftlub  11129  efsep  11130  effsumlt  11131  tanval3ap  11154  efi4p  11157  resin4p  11158  recos4p  11159  ef01bndlem  11196  sin01bnd  11197  cos01bnd  11198  sin01gt0  11201  cos01gt0  11202  absefib  11209  efieq1re  11210  eirraplem  11213  dvdsdc  11231  dvdscmulr  11252  dvdslelemd  11271  odd2np1lem  11299  odd2np1  11300  flodddiv4  11361  gcdsupex  11376  gcdsupcl  11377  gcd1  11405  nn0seqcvgd  11450  algcvg  11457  algcvgblem  11458  eucalg  11468  prmind2  11529  qden1elz  11610  dfphi2  11623  phiprm  11626  phimullem  11628  oddennn  11632  xpct  11636  restid  11815  restuni2  12029  cnrest2r  12088  lmfss  12095  lmres  12099  lmtopcnp  12101  ispsmet  12109  isxmet2d  12134  ismet2  12140  blfvalps  12171  blex  12173  xblss2  12191  climcncf  12337  nninfsellemdc  12607