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  3274  ssdifin0  3573  uneqdifeqim  3577  unimax  3921  opth  4322  djussxp  4864  iss  5047  relresfld  5254  eldmrexrn  5769  f1oresrab  5793  fmptco  5794  fsn  5800  fnressn  5818  foima2  5868  foeqcnvco  5907  isoini2  5936  ofres  6223  ofco  6227  tposexg  6394  tfrlemisucaccv  6461  tfrlemibex  6465  tfri1dALT  6487  tfrcl  6500  rdgivallem  6517  frecabex  6534  frectfr  6536  frecrdg  6544  pmresg  6813  mapsn  6827  mapsncnv  6832  ixpsnf1o  6873  en1  6941  2dom  6948  enpr2d  6962  en2  6963  mapxpen  6997  phplem4  7004  exmidpw2en  7062  fiintim  7081  sbthlem2  7113  elfir  7128  infglbti  7180  caseinl  7246  caseinr  7247  difinfsnlem  7254  difinfsn  7255  nninfisollemne  7286  exmidfodomrlemim  7367  exmidfodomrlemr  7368  exmidfodomrlemrALT  7369  2omotaplemap  7431  archnqq  7592  prarloclemlt  7668  prarloclemlo  7669  prarloclemcalc  7677  recexprlemm  7799  recexprlemex  7812  caucvgprlemm  7843  caucvgprprlemmu  7870  suplocexprlem2b  7889  suplocexprlemmu  7893  suplocexprlemlub  7899  1idsr  7943  recexgt0sr  7948  archsr  7957  caucvgsrlemoffval  7971  caucvgsrlemofff  7972  caucvgsrlemoffres  7975  caucvgsr  7977  ltpsrprg  7978  suplocsrlem  7983  pitonnlem2  8022  pitonn  8023  pitoregt0  8024  pitore  8025  recnnre  8026  axrnegex  8054  nntopi  8069  msqge0  8751  mulge0  8754  recexaplem2  8787  recexap  8788  recgt0  8985  recreclt  9035  nn1m1nn  9116  nn1suc  9117  nnle1eq1  9122  nn1gt1  9132  nnsub  9137  addltmul  9336  nn0le0eq0  9385  elnn0nn  9399  elnnz  9444  elznn0  9449  zlem1lt  9491  zltlem1  9492  elz2  9506  nn0n0n1ge2b  9514  nn0lt2  9516  nn0le2is012  9517  eluzaddi  9737  eluzsubi  9738  uzp1  9744  peano2uzr  9768  nn01to3  9800  qreccl  9825  irrmulap  9831  ltpnf  9964  xaddass2  10054  iccen  10190  fz01en  10237  fzpreddisj  10255  fzsuc2  10263  fseq1p1m1  10278  fseq1m1p1  10279  elfzp1b  10281  fzoss2  10358  fzval3  10397  fzosplitsnm1  10402  fzosplitprm1  10427  flhalf  10509  fldiv4lem1div2uz2  10513  modqmulnn  10551  modqmuladdnn0  10577  frec2uzrand  10614  frecuzrdg0  10622  frecuzrdg0t  10631  frecfzennn  10635  frecfzen2  10636  uzennn  10645  seqeq1  10659  seqp1g  10675  seqclg  10681  seq3m1  10682  monoord2  10695  ser3mono  10696  seqf1oglem1  10728  seqf1oglem2  10729  seqfeq4g  10740  ser0f  10743  exp3vallem  10749  expm1t  10776  expeq0  10779  expubnd  10805  binom3  10866  facndiv  10948  facavg  10955  bcn0  10964  bcnp1n  10968  bcm1k  10969  bcp1nk  10971  bcval5  10972  bcn2  10973  bcp1m1  10974  bcpasc  10975  bcn2m1  10978  hashsng  11007  hashun  11014  hashfz  11030  hashfzo  11031  seq3coll  11051  hash2en  11052  iswrdiz  11065  snopiswrd  11068  ccat1st1st  11158  swrds1  11186  cats1un  11239  wrdind  11240  wrd2ind  11241  swrdccatin1  11243  swrdccat3blem  11257  shftfval  11318  2shfti  11328  resqrexlemf1  11505  abs00ap  11559  sqabs  11579  ltabs  11584  caubnd2  11614  max0addsup  11716  rexico  11718  mulcn2  11809  climaddc1  11826  climmulc2  11828  climsubc1  11829  climsubc2  11830  iserex  11836  climlec2  11838  iser3shft  11843  climcvg1nlem  11846  serf0  11849  sumrbdc  11876  fsumm1  11913  fsump1  11917  fsum00  11959  telfsumo  11963  fsumparts  11967  hashiun  11975  binomlem  11980  binom1dif  11984  bcxmas  11986  isumsplit  11988  isum1p  11989  arisum  11995  arisum2  11996  trireciplem  11997  explecnv  12002  geolim  12008  georeclim  12010  mertenslem2  12033  mertensabs  12034  prodf1f  12040  prodrbdclem2  12070  efcllemp  12155  ef0lem  12157  efgt0  12181  eftlub  12187  efsep  12188  effsumlt  12189  tanval3ap  12211  efi4p  12214  resin4p  12215  recos4p  12216  ef01bndlem  12253  sin01bnd  12254  cos01bnd  12255  sinltxirr  12258  sin01gt0  12259  cos01gt0  12260  absefib  12268  efieq1re  12269  eirraplem  12274  dvdsdc  12295  dvdscmulr  12317  fsumdvds  12339  dvdslelemd  12340  3dvds  12361  odd2np1lem  12369  odd2np1  12370  flodddiv4  12433  bitsfzo  12452  bitsmod  12453  gcdsupex  12464  gcdsupcl  12465  gcd1  12494  nninfctlemfo  12547  nn0seqcvgd  12549  algcvg  12556  algcvgblem  12557  eucalg  12567  prmind2  12628  qden1elz  12713  dfphi2  12728  phiprm  12731  phimullem  12733  prmdiv  12743  prmdiveq  12744  prm23lt5  12772  pcpre1  12801  pczpre  12806  pcdiv  12811  pc1  12814  pcqdiv  12816  pcexp  12818  pcxnn0cl  12819  pcxcl  12820  pcdvdstr  12836  pc2dvds  12839  sumhashdc  12856  fldivp1  12857  pcfaclem  12858  qexpz  12861  expnprm  12862  prmpwdvds  12864  pockthlem  12865  4sqlem5  12891  4sqlem6  12892  4sqlem11  12910  4sqlem13m  12912  4sqlem19  12918  oddennn  12949  xpct  12953  ennnfonelemj0  12958  ennnfonelemen  12978  ctinfomlemom  12984  omctfn  13000  restid  13269  prdsex  13288  prdsval  13292  prdsbaslemss  13293  prdsbas  13295  imasbas  13326  imasplusg  13327  imasmulr  13328  imasaddfnlemg  13333  xpscf  13366  igsumvalx  13408  gsumsplit1r  13417  gsumprval  13418  gsumfzz  13514  gsumfzcl  13518  prdsgrpd  13628  prdsinvgd  13629  mulgnngsum  13650  mulgnndir  13674  mulgneg2  13679  dvdsrmuld  14045  zsssubrg  14534  znval  14585  znle  14586  znbaslemnn  14588  znf1o  14600  znleval  14602  psrval  14615  restuni2  14836  cnrest2r  14896  lmfss  14903  lmres  14907  lmtopcnp  14909  ispsmet  14982  isxmet2d  15007  ismet2  15013  blfvalps  15044  blex  15046  xblss2  15064  reopnap  15205  divcnap  15224  climcncf  15243  cncfmpt2fcntop  15258  hovera  15306  limcdifap  15321  cnplimcim  15326  cnlimcim  15330  cnlimc  15331  cnlimci  15332  dvbss  15344  dvcnp2cntop  15358  dvcn  15359  dvaddxxbr  15360  dvmulxxbr  15361  dvexp  15370  dveflem  15385  plyval  15391  elply2  15394  plyf  15396  plyss  15397  plyssc  15398  elplyr  15399  plyaddlem1  15406  plymullem1  15407  plyaddlem  15408  plymullem  15409  plyco  15418  plycj  15420  dvply1  15424  reeff1olem  15430  sinperlem  15467  sin2kpi  15470  cos2kpi  15471  sin2pim  15472  cos2pim  15473  cosq14gt0  15491  coseq0q4123  15493  tangtx  15497  abssinper  15505  sinkpi  15506  coskpi  15507  cosq34lt1  15509  logrpap0b  15535  logdivlti  15540  rpcxpsqrtth  15589  rpabscxpbnd  15599  binom4  15638  wilthlem1  15639  0sgm  15644  1sgmprm  15653  1sgm2ppw  15654  mersenne  15656  perfect1  15657  perfectlem1  15658  perfectlem2  15659  perfect  15660  lgslem1  15664  lgsval  15668  lgsfvalg  15669  lgsfcl2  15670  lgsfcl  15672  lgsval2lem  15674  lgsvalmod  15683  lgsneg  15688  lgsdilem  15691  lgsdir2lem3  15694  lgsdir  15699  lgsdilem2  15700  lgsdi  15701  lgsne0  15702  lgsabs1  15703  lgsprme0  15706  lgsdirnn0  15711  lgsdinn0  15712  gausslemma2dlem0d  15716  gausslemma2dlem1a  15722  gausslemma2dlem1f1o  15724  gausslemma2dlem3  15727  gausslemma2dlem4  15728  gausslemma2dlem5a  15729  gausslemma2dlem5  15730  gausslemma2dlem6  15731  lgseisenlem2  15735  lgseisen  15738  lgsquadlem1  15741  lgsquadlem2  15742  lgsquad2lem1  15745  lgsquad2lem2  15746  lgsquad2  15747  m1lgs  15749  2lgslem1  15755  2lgslem2  15756  2lgs  15768  2sqlem9  15788  2sqlem10  15789  ushgredgedg  16009  ushgredgedgloop  16011  2omap  16290  pwle2  16295  pw1nct  16300  nninfsellemdc  16307  nnnninfen  16318  nnnninfex  16319  nninfnfiinf  16320  sbthom  16325  trirec0  16343  apdifflemr  16346  reap0  16357  nconstwlpolem  16364