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  1807  sseqtrid  3277  ssdifin0  3576  uneqdifeqim  3580  unimax  3927  opth  4329  djussxp  4875  iss  5059  relresfld  5266  eldmrexrn  5788  f1oresrab  5812  fmptco  5813  fsn  5819  fnressn  5840  foima2  5892  foeqcnvco  5931  isoini2  5960  relmptopab  6224  ofres  6250  ofco  6254  tposexg  6424  tfrlemisucaccv  6491  tfrlemibex  6495  tfri1dALT  6517  tfrcl  6530  rdgivallem  6547  frecabex  6564  frectfr  6566  frecrdg  6574  pmresg  6845  mapsn  6859  mapsncnv  6864  ixpsnf1o  6905  en1  6973  2dom  6980  enpr2d  6997  en2  6998  mapxpen  7034  phplem4  7041  exmidpw2en  7104  fiintim  7123  sbthlem2  7157  elfir  7172  infglbti  7224  caseinl  7290  caseinr  7291  difinfsnlem  7298  difinfsn  7299  nninfisollemne  7330  exmidfodomrlemim  7412  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  2omotaplemap  7476  archnqq  7637  prarloclemlt  7713  prarloclemlo  7714  prarloclemcalc  7722  recexprlemm  7844  recexprlemex  7857  caucvgprlemm  7888  caucvgprprlemmu  7915  suplocexprlem2b  7934  suplocexprlemmu  7938  suplocexprlemlub  7944  1idsr  7988  recexgt0sr  7993  archsr  8002  caucvgsrlemoffval  8016  caucvgsrlemofff  8017  caucvgsrlemoffres  8020  caucvgsr  8022  ltpsrprg  8023  suplocsrlem  8028  pitonnlem2  8067  pitonn  8068  pitoregt0  8069  pitore  8070  recnnre  8071  axrnegex  8099  nntopi  8114  msqge0  8796  mulge0  8799  recexaplem2  8832  recexap  8833  recgt0  9030  recreclt  9080  nn1m1nn  9161  nn1suc  9162  nnle1eq1  9167  nn1gt1  9177  nnsub  9182  addltmul  9381  nn0le0eq0  9430  elnn0nn  9444  elnnz  9489  elznn0  9494  zlem1lt  9536  zltlem1  9537  elz2  9551  nn0n0n1ge2b  9559  nn0lt2  9561  nn0le2is012  9562  eluzaddi  9783  eluzsubi  9784  uzp1  9790  peano2uzr  9819  nn01to3  9851  qreccl  9876  irrmulap  9882  ltpnf  10015  xaddass2  10105  iccen  10241  fz01en  10288  fzpreddisj  10306  fzsuc2  10314  fseq1p1m1  10329  fseq1m1p1  10330  elfzp1b  10332  fzoss2  10409  fzval3  10450  fzosplitsnm1  10455  fzosplitprm1  10481  flhalf  10563  fldiv4lem1div2uz2  10567  modqmulnn  10605  modqmuladdnn0  10631  frec2uzrand  10668  frecuzrdg0  10676  frecuzrdg0t  10685  frecfzennn  10689  frecfzen2  10690  uzennn  10699  seqeq1  10713  seqp1g  10729  seqclg  10735  seq3m1  10736  monoord2  10749  ser3mono  10750  seqf1oglem1  10782  seqf1oglem2  10783  seqfeq4g  10794  ser0f  10797  exp3vallem  10803  expm1t  10830  expeq0  10833  expubnd  10859  binom3  10920  facndiv  11002  facavg  11009  bcn0  11018  bcnp1n  11022  bcm1k  11023  bcp1nk  11025  bcval5  11026  bcn2  11027  bcp1m1  11028  bcpasc  11029  bcn2m1  11032  hashsng  11061  hashun  11069  hashfz  11086  hashfzo  11087  seq3coll  11107  hash2en  11108  iswrdiz  11124  snopiswrd  11127  ccat1st1st  11222  swrds1  11253  cats1un  11306  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  swrdccat3blem  11324  shftfval  11386  2shfti  11396  resqrexlemf1  11573  abs00ap  11627  sqabs  11647  ltabs  11652  caubnd2  11682  max0addsup  11784  rexico  11786  mulcn2  11877  climaddc1  11894  climmulc2  11896  climsubc1  11897  climsubc2  11898  iserex  11904  climlec2  11906  iser3shft  11911  climcvg1nlem  11914  serf0  11917  sumrbdc  11945  fsumm1  11982  fsump1  11986  fsum00  12028  telfsumo  12032  fsumparts  12036  hashiun  12044  binomlem  12049  binom1dif  12053  bcxmas  12055  isumsplit  12057  isum1p  12058  arisum  12064  arisum2  12065  trireciplem  12066  explecnv  12071  geolim  12077  georeclim  12079  mertenslem2  12102  mertensabs  12103  prodf1f  12109  prodrbdclem2  12139  efcllemp  12224  ef0lem  12226  efgt0  12250  eftlub  12256  efsep  12257  effsumlt  12258  tanval3ap  12280  efi4p  12283  resin4p  12284  recos4p  12285  ef01bndlem  12322  sin01bnd  12323  cos01bnd  12324  sinltxirr  12327  sin01gt0  12328  cos01gt0  12329  absefib  12337  efieq1re  12338  eirraplem  12343  dvdsdc  12364  dvdscmulr  12386  fsumdvds  12408  dvdslelemd  12409  3dvds  12430  odd2np1lem  12438  odd2np1  12439  flodddiv4  12502  bitsfzo  12521  bitsmod  12522  gcdsupex  12533  gcdsupcl  12534  gcd1  12563  nninfctlemfo  12616  nn0seqcvgd  12618  algcvg  12625  algcvgblem  12626  eucalg  12636  prmind2  12697  qden1elz  12782  dfphi2  12797  phiprm  12800  phimullem  12802  prmdiv  12812  prmdiveq  12813  prm23lt5  12841  pcpre1  12870  pczpre  12875  pcdiv  12880  pc1  12883  pcqdiv  12885  pcexp  12887  pcxnn0cl  12888  pcxcl  12889  pcdvdstr  12905  pc2dvds  12908  sumhashdc  12925  fldivp1  12926  pcfaclem  12927  qexpz  12930  expnprm  12931  prmpwdvds  12933  pockthlem  12934  4sqlem5  12960  4sqlem6  12961  4sqlem11  12979  4sqlem13m  12981  4sqlem19  12987  oddennn  13018  xpct  13022  ennnfonelemj0  13027  ennnfonelemen  13047  ctinfomlemom  13053  omctfn  13069  restid  13338  prdsex  13357  prdsval  13361  prdsbaslemss  13362  prdsbas  13364  imasbas  13395  imasplusg  13396  imasmulr  13397  imasaddfnlemg  13402  xpscf  13435  igsumvalx  13477  gsumsplit1r  13486  gsumprval  13487  gsumfzz  13583  gsumfzcl  13587  prdsgrpd  13697  prdsinvgd  13698  mulgnngsum  13719  mulgnndir  13743  mulgneg2  13748  dvdsrmuld  14116  zsssubrg  14605  znval  14656  znle  14657  znbaslemnn  14659  znf1o  14671  znleval  14673  psrval  14686  restuni2  14907  cnrest2r  14967  lmfss  14974  lmres  14978  lmtopcnp  14980  ispsmet  15053  isxmet2d  15078  ismet2  15084  blfvalps  15115  blex  15117  xblss2  15135  reopnap  15276  divcnap  15295  climcncf  15314  cncfmpt2fcntop  15329  hovera  15377  limcdifap  15392  cnplimcim  15397  cnlimcim  15401  cnlimc  15402  cnlimci  15403  dvbss  15415  dvcnp2cntop  15429  dvcn  15430  dvaddxxbr  15431  dvmulxxbr  15432  dvexp  15441  dveflem  15456  plyval  15462  elply2  15465  plyf  15467  plyss  15468  plyssc  15469  elplyr  15470  plyaddlem1  15477  plymullem1  15478  plyaddlem  15479  plymullem  15480  plyco  15489  plycj  15491  dvply1  15495  reeff1olem  15501  sinperlem  15538  sin2kpi  15541  cos2kpi  15542  sin2pim  15543  cos2pim  15544  cosq14gt0  15562  coseq0q4123  15564  tangtx  15568  abssinper  15576  sinkpi  15577  coskpi  15578  cosq34lt1  15580  logrpap0b  15606  logdivlti  15611  rpcxpsqrtth  15660  rpabscxpbnd  15670  binom4  15709  wilthlem1  15710  0sgm  15715  1sgmprm  15724  1sgm2ppw  15725  mersenne  15727  perfect1  15728  perfectlem1  15729  perfectlem2  15730  perfect  15731  lgslem1  15735  lgsval  15739  lgsfvalg  15740  lgsfcl2  15741  lgsfcl  15743  lgsval2lem  15745  lgsvalmod  15754  lgsneg  15759  lgsdilem  15762  lgsdir2lem3  15765  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  lgsabs1  15774  lgsprme0  15777  lgsdirnn0  15782  lgsdinn0  15783  gausslemma2dlem0d  15787  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem3  15798  gausslemma2dlem4  15799  gausslemma2dlem5a  15800  gausslemma2dlem5  15801  gausslemma2dlem6  15802  lgseisenlem2  15806  lgseisen  15809  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem1  15816  lgsquad2lem2  15817  lgsquad2  15818  m1lgs  15820  2lgslem1  15826  2lgslem2  15827  2lgs  15839  2sqlem9  15859  2sqlem10  15860  ushgredgedg  16083  ushgredgedgloop  16085  uhgrspansubgrlem  16133  wlkvtxiedg  16202  wlkvtxiedgg  16203  wlk1walkdom  16216  upgr2wlkdc  16234  clwwlkccatlem  16257  umgrclwwlkge2  16259  clwwlknonmpo  16285  clwwlknonex2lem2  16295  clwwlknonex2  16296  2omap  16620  pwle2  16625  pw1nct  16630  nninfsellemdc  16638  nnnninfen  16649  nnnninfex  16650  nninfnfiinf  16651  sbthom  16656  trirec0  16674  apdifflemr  16677  reap0  16688  nconstwlpolem  16695  gfsumval  16706