Theorem sylancl 404

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

Hypotheses

Ref	Expression
sylancl.1	⊢ (𝜑 → 𝜓)
sylancl.2	⊢ 𝜒
sylancl.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylancl	⊢ (𝜑 → 𝜃)

Proof of Theorem sylancl

Step	Hyp	Ref	Expression
1		sylancl.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylancl.2	. . 3 ⊢ 𝜒
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝜒)
4		sylancl.3	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 3, 4	syl2anc 403	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  sylanblc  406  sylanblrc  407  equveli  1686  syl5sseq  3063  ssdifin0  3351  uneqdifeqim  3355  unimax  3670  opth  4038  djussxp  4549  iss  4725  relresfld  4926  eldmrexrn  5403  f1oresrab  5426  fmptco  5427  fsn  5432  fnressn  5446  foima2  5491  foeqcnvco  5530  isoini2  5559  ofres  5826  ofco  5830  tposexg  5977  tfrlemisucaccv  6044  tfrlemibex  6048  tfri1dALT  6070  tfrcl  6083  rdgivallem  6100  frecabex  6117  frectfr  6119  frecrdg  6127  pmresg  6385  mapsn  6399  mapsncnv  6404  en1  6468  2dom  6474  mapxpen  6516  phplem4  6523  sbthlem2  6611  infglbti  6664  exmidfodomrlemim  6771  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  archnqq  6920  prarloclemlt  6996  prarloclemlo  6997  prarloclemcalc  7005  recexprlemm  7127  recexprlemex  7140  caucvgprlemm  7171  caucvgprprlemmu  7198  1idsr  7258  recexgt0sr  7263  archsr  7271  caucvgsrlemoffval  7285  caucvgsrlemofff  7286  caucvgsrlemoffres  7289  caucvgsr  7291  pitonnlem2  7328  pitonn  7329  pitoregt0  7330  pitore  7331  recnnre  7332  axrnegex  7358  nntopi  7373  msqge0  8034  mulge0  8037  recexaplem2  8060  recexap  8061  recgt0  8246  recreclt  8296  nn1m1nn  8375  nn1suc  8376  nnle1eq1  8381  nn1gt1  8390  nnsub  8395  addltmul  8585  nn0le0eq0  8634  elnn0nn  8648  elnnz  8693  elznn0  8698  zlem1lt  8739  zltlem1  8740  elz2  8751  nn0n0n1ge2b  8759  nn0lt2  8761  eluzaddi  8977  eluzsubi  8978  uzp1  8984  peano2uzr  9005  nn01to3  9034  qreccl  9059  ltpnf  9183  fz01en  9399  fzpreddisj  9415  fzsuc2  9423  fseq1p1m1  9438  fseq1m1p1  9439  elfzp1b  9441  fzoss2  9511  fzval3  9543  fzosplitsnm1  9548  fzosplitprm1  9573  flhalf  9637  modqmulnn  9677  modqmuladdnn0  9703  frec2uzrand  9740  frecuzrdg0  9748  frecuzrdg0t  9757  frecfzennn  9761  frecfzen2  9762  iseqeq1  9782  iseqm1  9801  monoord2  9810  isermono  9811  iser0f  9848  expm1t  9881  expeq0  9884  expubnd  9910  binom3  9967  facndiv  10043  facavg  10050  bcn0  10059  bcnp1n  10063  bcm1k  10064  bcp1nk  10066  ibcval5  10067  bcn2  10068  bcp1m1  10069  bcpasc  10070  bcn2m1  10073  hashsng  10102  hashun  10109  hashfz  10125  hashfzo  10126  iseqcoll  10143  shftfval  10151  2shfti  10161  resqrexlemf1  10336  abs00ap  10390  abs00  10392  sqabs  10410  ltabs  10415  caubnd2  10445  max0addsup  10547  rexico  10549  mulcn2  10593  climaddc1  10609  climmulc2  10611  climsubc1  10612  climsubc2  10613  iiserex  10619  climlec2  10621  climcvg1nlem  10628  serif0  10631  isumrb  10657  dvdsdc  10679  dvdscmulr  10700  dvdslelemd  10719  odd2np1lem  10747  odd2np1  10748  flodddiv4  10809  gcdsupex  10824  gcdsupcl  10825  gcd1  10853  nn0seqcvgd  10898  ialgcvg  10905  algcvgblem  10906  eucialg  10916  prmind2  10977  qden1elz  11058  dfphi2  11071  phiprm  11074  phimullem  11076  oddennn  11080  xpct  11084  nninfsellemdc  11340