Theorem sylancl 413

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 411	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  sylanblc  415  sylanblrc  416  equveli  1805  sseqtrid  3275  ssdifin0  3574  uneqdifeqim  3578  unimax  3925  opth  4327  djussxp  4873  iss  5057  relresfld  5264  eldmrexrn  5784  f1oresrab  5808  fmptco  5809  fsn  5815  fnressn  5835  foima2  5887  foeqcnvco  5926  isoini2  5955  relmptopab  6219  ofres  6245  ofco  6249  tposexg  6419  tfrlemisucaccv  6486  tfrlemibex  6490  tfri1dALT  6512  tfrcl  6525  rdgivallem  6542  frecabex  6559  frectfr  6561  frecrdg  6569  pmresg  6840  mapsn  6854  mapsncnv  6859  ixpsnf1o  6900  en1  6968  2dom  6975  enpr2d  6992  en2  6993  mapxpen  7029  phplem4  7036  exmidpw2en  7099  fiintim  7118  sbthlem2  7151  elfir  7166  infglbti  7218  caseinl  7284  caseinr  7285  difinfsnlem  7292  difinfsn  7293  nninfisollemne  7324  exmidfodomrlemim  7405  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  2omotaplemap  7469  archnqq  7630  prarloclemlt  7706  prarloclemlo  7707  prarloclemcalc  7715  recexprlemm  7837  recexprlemex  7850  caucvgprlemm  7881  caucvgprprlemmu  7908  suplocexprlem2b  7927  suplocexprlemmu  7931  suplocexprlemlub  7937  1idsr  7981  recexgt0sr  7986  archsr  7995  caucvgsrlemoffval  8009  caucvgsrlemofff  8010  caucvgsrlemoffres  8013  caucvgsr  8015  ltpsrprg  8016  suplocsrlem  8021  pitonnlem2  8060  pitonn  8061  pitoregt0  8062  pitore  8063  recnnre  8064  axrnegex  8092  nntopi  8107  msqge0  8789  mulge0  8792  recexaplem2  8825  recexap  8826  recgt0  9023  recreclt  9073  nn1m1nn  9154  nn1suc  9155  nnle1eq1  9160  nn1gt1  9170  nnsub  9175  addltmul  9374  nn0le0eq0  9423  elnn0nn  9437  elnnz  9482  elznn0  9487  zlem1lt  9529  zltlem1  9530  elz2  9544  nn0n0n1ge2b  9552  nn0lt2  9554  nn0le2is012  9555  eluzaddi  9776  eluzsubi  9777  uzp1  9783  peano2uzr  9812  nn01to3  9844  qreccl  9869  irrmulap  9875  ltpnf  10008  xaddass2  10098  iccen  10234  fz01en  10281  fzpreddisj  10299  fzsuc2  10307  fseq1p1m1  10322  fseq1m1p1  10323  elfzp1b  10325  fzoss2  10402  fzval3  10442  fzosplitsnm1  10447  fzosplitprm1  10473  flhalf  10555  fldiv4lem1div2uz2  10559  modqmulnn  10597  modqmuladdnn0  10623  frec2uzrand  10660  frecuzrdg0  10668  frecuzrdg0t  10677  frecfzennn  10681  frecfzen2  10682  uzennn  10691  seqeq1  10705  seqp1g  10721  seqclg  10727  seq3m1  10728  monoord2  10741  ser3mono  10742  seqf1oglem1  10774  seqf1oglem2  10775  seqfeq4g  10786  ser0f  10789  exp3vallem  10795  expm1t  10822  expeq0  10825  expubnd  10851  binom3  10912  facndiv  10994  facavg  11001  bcn0  11010  bcnp1n  11014  bcm1k  11015  bcp1nk  11017  bcval5  11018  bcn2  11019  bcp1m1  11020  bcpasc  11021  bcn2m1  11024  hashsng  11053  hashun  11061  hashfz  11078  hashfzo  11079  seq3coll  11099  hash2en  11100  iswrdiz  11113  snopiswrd  11116  ccat1st1st  11211  swrds1  11242  cats1un  11295  wrdind  11296  wrd2ind  11297  swrdccatin1  11299  swrdccat3blem  11313  shftfval  11375  2shfti  11385  resqrexlemf1  11562  abs00ap  11616  sqabs  11636  ltabs  11641  caubnd2  11671  max0addsup  11773  rexico  11775  mulcn2  11866  climaddc1  11883  climmulc2  11885  climsubc1  11886  climsubc2  11887  iserex  11893  climlec2  11895  iser3shft  11900  climcvg1nlem  11903  serf0  11906  sumrbdc  11933  fsumm1  11970  fsump1  11974  fsum00  12016  telfsumo  12020  fsumparts  12024  hashiun  12032  binomlem  12037  binom1dif  12041  bcxmas  12043  isumsplit  12045  isum1p  12046  arisum  12052  arisum2  12053  trireciplem  12054  explecnv  12059  geolim  12065  georeclim  12067  mertenslem2  12090  mertensabs  12091  prodf1f  12097  prodrbdclem2  12127  efcllemp  12212  ef0lem  12214  efgt0  12238  eftlub  12244  efsep  12245  effsumlt  12246  tanval3ap  12268  efi4p  12271  resin4p  12272  recos4p  12273  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  sinltxirr  12315  sin01gt0  12316  cos01gt0  12317  absefib  12325  efieq1re  12326  eirraplem  12331  dvdsdc  12352  dvdscmulr  12374  fsumdvds  12396  dvdslelemd  12397  3dvds  12418  odd2np1lem  12426  odd2np1  12427  flodddiv4  12490  bitsfzo  12509  bitsmod  12510  gcdsupex  12521  gcdsupcl  12522  gcd1  12551  nninfctlemfo  12604  nn0seqcvgd  12606  algcvg  12613  algcvgblem  12614  eucalg  12624  prmind2  12685  qden1elz  12770  dfphi2  12785  phiprm  12788  phimullem  12790  prmdiv  12800  prmdiveq  12801  prm23lt5  12829  pcpre1  12858  pczpre  12863  pcdiv  12868  pc1  12871  pcqdiv  12873  pcexp  12875  pcxnn0cl  12876  pcxcl  12877  pcdvdstr  12893  pc2dvds  12896  sumhashdc  12913  fldivp1  12914  pcfaclem  12915  qexpz  12918  expnprm  12919  prmpwdvds  12921  pockthlem  12922  4sqlem5  12948  4sqlem6  12949  4sqlem11  12967  4sqlem13m  12969  4sqlem19  12975  oddennn  13006  xpct  13010  ennnfonelemj0  13015  ennnfonelemen  13035  ctinfomlemom  13041  omctfn  13057  restid  13326  prdsex  13345  prdsval  13349  prdsbaslemss  13350  prdsbas  13352  imasbas  13383  imasplusg  13384  imasmulr  13385  imasaddfnlemg  13390  xpscf  13423  igsumvalx  13465  gsumsplit1r  13474  gsumprval  13475  gsumfzz  13571  gsumfzcl  13575  prdsgrpd  13685  prdsinvgd  13686  mulgnngsum  13707  mulgnndir  13731  mulgneg2  13736  dvdsrmuld  14103  zsssubrg  14592  znval  14643  znle  14644  znbaslemnn  14646  znf1o  14658  znleval  14660  psrval  14673  restuni2  14894  cnrest2r  14954  lmfss  14961  lmres  14965  lmtopcnp  14967  ispsmet  15040  isxmet2d  15065  ismet2  15071  blfvalps  15102  blex  15104  xblss2  15122  reopnap  15263  divcnap  15282  climcncf  15301  cncfmpt2fcntop  15316  hovera  15364  limcdifap  15379  cnplimcim  15384  cnlimcim  15388  cnlimc  15389  cnlimci  15390  dvbss  15402  dvcnp2cntop  15416  dvcn  15417  dvaddxxbr  15418  dvmulxxbr  15419  dvexp  15428  dveflem  15443  plyval  15449  elply2  15452  plyf  15454  plyss  15455  plyssc  15456  elplyr  15457  plyaddlem1  15464  plymullem1  15465  plyaddlem  15466  plymullem  15467  plyco  15476  plycj  15478  dvply1  15482  reeff1olem  15488  sinperlem  15525  sin2kpi  15528  cos2kpi  15529  sin2pim  15530  cos2pim  15531  cosq14gt0  15549  coseq0q4123  15551  tangtx  15555  abssinper  15563  sinkpi  15564  coskpi  15565  cosq34lt1  15567  logrpap0b  15593  logdivlti  15598  rpcxpsqrtth  15647  rpabscxpbnd  15657  binom4  15696  wilthlem1  15697  0sgm  15702  1sgmprm  15711  1sgm2ppw  15712  mersenne  15714  perfect1  15715  perfectlem1  15716  perfectlem2  15717  perfect  15718  lgslem1  15722  lgsval  15726  lgsfvalg  15727  lgsfcl2  15728  lgsfcl  15730  lgsval2lem  15732  lgsvalmod  15741  lgsneg  15746  lgsdilem  15749  lgsdir2lem3  15752  lgsdir  15757  lgsdilem2  15758  lgsdi  15759  lgsne0  15760  lgsabs1  15761  lgsprme0  15764  lgsdirnn0  15769  lgsdinn0  15770  gausslemma2dlem0d  15774  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  gausslemma2dlem3  15785  gausslemma2dlem4  15786  gausslemma2dlem5a  15787  gausslemma2dlem5  15788  gausslemma2dlem6  15789  lgseisenlem2  15793  lgseisen  15796  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad2lem1  15803  lgsquad2lem2  15804  lgsquad2  15805  m1lgs  15807  2lgslem1  15813  2lgslem2  15814  2lgs  15826  2sqlem9  15846  2sqlem10  15847  ushgredgedg  16070  ushgredgedgloop  16072  wlkvtxiedg  16156  wlkvtxiedgg  16157  wlk1walkdom  16170  upgr2wlkdc  16186  clwwlkccatlem  16209  umgrclwwlkge2  16211  clwwlknonmpo  16237  clwwlknonex2lem2  16247  clwwlknonex2  16248  2omap  16544  pwle2  16549  pw1nct  16554  nninfsellemdc  16562  nnnninfen  16573  nnnninfex  16574  nninfnfiinf  16575  sbthom  16580  trirec0  16598  apdifflemr  16601  reap0  16612  nconstwlpolem  16619  gfsumval  16630