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  1783  sseqtrid  3245  ssdifin0  3544  uneqdifeqim  3548  unimax  3887  opth  4286  djussxp  4828  iss  5011  relresfld  5218  eldmrexrn  5731  f1oresrab  5755  fmptco  5756  fsn  5762  fnressn  5780  foima2  5830  foeqcnvco  5869  isoini2  5898  ofres  6183  ofco  6187  tposexg  6354  tfrlemisucaccv  6421  tfrlemibex  6425  tfri1dALT  6447  tfrcl  6460  rdgivallem  6477  frecabex  6494  frectfr  6496  frecrdg  6504  pmresg  6773  mapsn  6787  mapsncnv  6792  ixpsnf1o  6833  en1  6901  2dom  6908  enpr2d  6922  en2  6923  mapxpen  6957  phplem4  6964  exmidpw2en  7021  fiintim  7040  sbthlem2  7072  elfir  7087  infglbti  7139  caseinl  7205  caseinr  7206  difinfsnlem  7213  difinfsn  7214  nninfisollemne  7245  exmidfodomrlemim  7322  exmidfodomrlemr  7323  exmidfodomrlemrALT  7324  2omotaplemap  7382  archnqq  7543  prarloclemlt  7619  prarloclemlo  7620  prarloclemcalc  7628  recexprlemm  7750  recexprlemex  7763  caucvgprlemm  7794  caucvgprprlemmu  7821  suplocexprlem2b  7840  suplocexprlemmu  7844  suplocexprlemlub  7850  1idsr  7894  recexgt0sr  7899  archsr  7908  caucvgsrlemoffval  7922  caucvgsrlemofff  7923  caucvgsrlemoffres  7926  caucvgsr  7928  ltpsrprg  7929  suplocsrlem  7934  pitonnlem2  7973  pitonn  7974  pitoregt0  7975  pitore  7976  recnnre  7977  axrnegex  8005  nntopi  8020  msqge0  8702  mulge0  8705  recexaplem2  8738  recexap  8739  recgt0  8936  recreclt  8986  nn1m1nn  9067  nn1suc  9068  nnle1eq1  9073  nn1gt1  9083  nnsub  9088  addltmul  9287  nn0le0eq0  9336  elnn0nn  9350  elnnz  9395  elznn0  9400  zlem1lt  9442  zltlem1  9443  elz2  9457  nn0n0n1ge2b  9465  nn0lt2  9467  nn0le2is012  9468  eluzaddi  9688  eluzsubi  9689  uzp1  9695  peano2uzr  9719  nn01to3  9751  qreccl  9776  irrmulap  9782  ltpnf  9915  xaddass2  10005  iccen  10141  fz01en  10188  fzpreddisj  10206  fzsuc2  10214  fseq1p1m1  10229  fseq1m1p1  10230  elfzp1b  10232  fzoss2  10309  fzval3  10346  fzosplitsnm1  10351  fzosplitprm1  10376  flhalf  10458  fldiv4lem1div2uz2  10462  modqmulnn  10500  modqmuladdnn0  10526  frec2uzrand  10563  frecuzrdg0  10571  frecuzrdg0t  10580  frecfzennn  10584  frecfzen2  10585  uzennn  10594  seqeq1  10608  seqp1g  10624  seqclg  10630  seq3m1  10631  monoord2  10644  ser3mono  10645  seqf1oglem1  10677  seqf1oglem2  10678  seqfeq4g  10689  ser0f  10692  exp3vallem  10698  expm1t  10725  expeq0  10728  expubnd  10754  binom3  10815  facndiv  10897  facavg  10904  bcn0  10913  bcnp1n  10917  bcm1k  10918  bcp1nk  10920  bcval5  10921  bcn2  10922  bcp1m1  10923  bcpasc  10924  bcn2m1  10927  hashsng  10956  hashun  10963  hashfz  10979  hashfzo  10980  seq3coll  11000  hash2en  11001  iswrdiz  11014  snopiswrd  11017  ccat1st1st  11107  swrds1  11135  shftfval  11182  2shfti  11192  resqrexlemf1  11369  abs00ap  11423  sqabs  11443  ltabs  11448  caubnd2  11478  max0addsup  11580  rexico  11582  mulcn2  11673  climaddc1  11690  climmulc2  11692  climsubc1  11693  climsubc2  11694  iserex  11700  climlec2  11702  iser3shft  11707  climcvg1nlem  11710  serf0  11713  sumrbdc  11740  fsumm1  11777  fsump1  11781  fsum00  11823  telfsumo  11827  fsumparts  11831  hashiun  11839  binomlem  11844  binom1dif  11848  bcxmas  11850  isumsplit  11852  isum1p  11853  arisum  11859  arisum2  11860  trireciplem  11861  explecnv  11866  geolim  11872  georeclim  11874  mertenslem2  11897  mertensabs  11898  prodf1f  11904  prodrbdclem2  11934  efcllemp  12019  ef0lem  12021  efgt0  12045  eftlub  12051  efsep  12052  effsumlt  12053  tanval3ap  12075  efi4p  12078  resin4p  12079  recos4p  12080  ef01bndlem  12117  sin01bnd  12118  cos01bnd  12119  sinltxirr  12122  sin01gt0  12123  cos01gt0  12124  absefib  12132  efieq1re  12133  eirraplem  12138  dvdsdc  12159  dvdscmulr  12181  fsumdvds  12203  dvdslelemd  12204  3dvds  12225  odd2np1lem  12233  odd2np1  12234  flodddiv4  12297  bitsfzo  12316  bitsmod  12317  gcdsupex  12328  gcdsupcl  12329  gcd1  12358  nninfctlemfo  12411  nn0seqcvgd  12413  algcvg  12420  algcvgblem  12421  eucalg  12431  prmind2  12492  qden1elz  12577  dfphi2  12592  phiprm  12595  phimullem  12597  prmdiv  12607  prmdiveq  12608  prm23lt5  12636  pcpre1  12665  pczpre  12670  pcdiv  12675  pc1  12678  pcqdiv  12680  pcexp  12682  pcxnn0cl  12683  pcxcl  12684  pcdvdstr  12700  pc2dvds  12703  sumhashdc  12720  fldivp1  12721  pcfaclem  12722  qexpz  12725  expnprm  12726  prmpwdvds  12728  pockthlem  12729  4sqlem5  12755  4sqlem6  12756  4sqlem11  12774  4sqlem13m  12776  4sqlem19  12782  oddennn  12813  xpct  12817  ennnfonelemj0  12822  ennnfonelemen  12842  ctinfomlemom  12848  omctfn  12864  restid  13132  prdsex  13151  prdsval  13155  prdsbaslemss  13156  prdsbas  13158  imasbas  13189  imasplusg  13190  imasmulr  13191  imasaddfnlemg  13196  xpscf  13229  igsumvalx  13271  gsumsplit1r  13280  gsumprval  13281  gsumfzz  13377  gsumfzcl  13381  prdsgrpd  13491  prdsinvgd  13492  mulgnngsum  13513  mulgnndir  13537  mulgneg2  13542  dvdsrmuld  13908  zsssubrg  14397  znval  14448  znle  14449  znbaslemnn  14451  znf1o  14463  znleval  14465  psrval  14478  restuni2  14699  cnrest2r  14759  lmfss  14766  lmres  14770  lmtopcnp  14772  ispsmet  14845  isxmet2d  14870  ismet2  14876  blfvalps  14907  blex  14909  xblss2  14927  reopnap  15068  divcnap  15087  climcncf  15106  cncfmpt2fcntop  15121  hovera  15169  limcdifap  15184  cnplimcim  15189  cnlimcim  15193  cnlimc  15194  cnlimci  15195  dvbss  15207  dvcnp2cntop  15221  dvcn  15222  dvaddxxbr  15223  dvmulxxbr  15224  dvexp  15233  dveflem  15248  plyval  15254  elply2  15257  plyf  15259  plyss  15260  plyssc  15261  elplyr  15262  plyaddlem1  15269  plymullem1  15270  plyaddlem  15271  plymullem  15272  plyco  15281  plycj  15283  dvply1  15287  reeff1olem  15293  sinperlem  15330  sin2kpi  15333  cos2kpi  15334  sin2pim  15335  cos2pim  15336  cosq14gt0  15354  coseq0q4123  15356  tangtx  15360  abssinper  15368  sinkpi  15369  coskpi  15370  cosq34lt1  15372  logrpap0b  15398  logdivlti  15403  rpcxpsqrtth  15452  rpabscxpbnd  15462  binom4  15501  wilthlem1  15502  0sgm  15507  1sgmprm  15516  1sgm2ppw  15517  mersenne  15519  perfect1  15520  perfectlem1  15521  perfectlem2  15522  perfect  15523  lgslem1  15527  lgsval  15531  lgsfvalg  15532  lgsfcl2  15533  lgsfcl  15535  lgsval2lem  15537  lgsvalmod  15546  lgsneg  15551  lgsdilem  15554  lgsdir2lem3  15557  lgsdir  15562  lgsdilem2  15563  lgsdi  15564  lgsne0  15565  lgsabs1  15566  lgsprme0  15569  lgsdirnn0  15574  lgsdinn0  15575  gausslemma2dlem0d  15579  gausslemma2dlem1a  15585  gausslemma2dlem1f1o  15587  gausslemma2dlem3  15590  gausslemma2dlem4  15591  gausslemma2dlem5a  15592  gausslemma2dlem5  15593  gausslemma2dlem6  15594  lgseisenlem2  15598  lgseisen  15601  lgsquadlem1  15604  lgsquadlem2  15605  lgsquad2lem1  15608  lgsquad2lem2  15609  lgsquad2  15610  m1lgs  15612  2lgslem1  15618  2lgslem2  15619  2lgs  15631  2sqlem9  15651  2sqlem10  15652  2omap  16047  pwle2  16050  pw1nct  16055  nninfsellemdc  16062  nnnninfen  16073  nnnninfex  16074  nninfnfiinf  16075  sbthom  16080  trirec0  16098  apdifflemr  16101  reap0  16112  nconstwlpolem  16119