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  1773  sseqtrid  3234  ssdifin0  3533  uneqdifeqim  3537  unimax  3874  opth  4271  djussxp  4812  iss  4993  relresfld  5200  eldmrexrn  5704  f1oresrab  5728  fmptco  5729  fsn  5735  fnressn  5749  foima2  5799  foeqcnvco  5838  isoini2  5867  ofres  6152  ofco  6156  tposexg  6318  tfrlemisucaccv  6385  tfrlemibex  6389  tfri1dALT  6411  tfrcl  6424  rdgivallem  6441  frecabex  6458  frectfr  6460  frecrdg  6468  pmresg  6737  mapsn  6751  mapsncnv  6756  ixpsnf1o  6797  en1  6860  2dom  6866  enpr2d  6878  mapxpen  6911  phplem4  6918  exmidpw2en  6975  fiintim  6994  sbthlem2  7026  elfir  7041  infglbti  7093  caseinl  7159  caseinr  7160  difinfsnlem  7167  difinfsn  7168  nninfisollemne  7199  exmidfodomrlemim  7271  exmidfodomrlemr  7272  exmidfodomrlemrALT  7273  2omotaplemap  7327  archnqq  7487  prarloclemlt  7563  prarloclemlo  7564  prarloclemcalc  7572  recexprlemm  7694  recexprlemex  7707  caucvgprlemm  7738  caucvgprprlemmu  7765  suplocexprlem2b  7784  suplocexprlemmu  7788  suplocexprlemlub  7794  1idsr  7838  recexgt0sr  7843  archsr  7852  caucvgsrlemoffval  7866  caucvgsrlemofff  7867  caucvgsrlemoffres  7870  caucvgsr  7872  ltpsrprg  7873  suplocsrlem  7878  pitonnlem2  7917  pitonn  7918  pitoregt0  7919  pitore  7920  recnnre  7921  axrnegex  7949  nntopi  7964  msqge0  8646  mulge0  8649  recexaplem2  8682  recexap  8683  recgt0  8880  recreclt  8930  nn1m1nn  9011  nn1suc  9012  nnle1eq1  9017  nn1gt1  9027  nnsub  9032  addltmul  9231  nn0le0eq0  9280  elnn0nn  9294  elnnz  9339  elznn0  9344  zlem1lt  9385  zltlem1  9386  elz2  9400  nn0n0n1ge2b  9408  nn0lt2  9410  nn0le2is012  9411  eluzaddi  9631  eluzsubi  9632  uzp1  9638  peano2uzr  9662  nn01to3  9694  qreccl  9719  irrmulap  9725  ltpnf  9858  xaddass2  9948  iccen  10084  fz01en  10131  fzpreddisj  10149  fzsuc2  10157  fseq1p1m1  10172  fseq1m1p1  10173  elfzp1b  10175  fzoss2  10251  fzval3  10283  fzosplitsnm1  10288  fzosplitprm1  10313  flhalf  10395  fldiv4lem1div2uz2  10399  modqmulnn  10437  modqmuladdnn0  10463  frec2uzrand  10500  frecuzrdg0  10508  frecuzrdg0t  10517  frecfzennn  10521  frecfzen2  10522  uzennn  10531  seqeq1  10545  seqp1g  10561  seqclg  10567  seq3m1  10568  monoord2  10581  ser3mono  10582  seqf1oglem1  10614  seqf1oglem2  10615  seqfeq4g  10626  ser0f  10629  exp3vallem  10635  expm1t  10662  expeq0  10665  expubnd  10691  binom3  10752  facndiv  10834  facavg  10841  bcn0  10850  bcnp1n  10854  bcm1k  10855  bcp1nk  10857  bcval5  10858  bcn2  10859  bcp1m1  10860  bcpasc  10861  bcn2m1  10864  hashsng  10893  hashun  10900  hashfz  10916  hashfzo  10917  seq3coll  10937  iswrdiz  10945  snopiswrd  10948  shftfval  10989  2shfti  10999  resqrexlemf1  11176  abs00ap  11230  sqabs  11250  ltabs  11255  caubnd2  11285  max0addsup  11387  rexico  11389  mulcn2  11480  climaddc1  11497  climmulc2  11499  climsubc1  11500  climsubc2  11501  iserex  11507  climlec2  11509  iser3shft  11514  climcvg1nlem  11517  serf0  11520  sumrbdc  11547  fsumm1  11584  fsump1  11588  fsum00  11630  telfsumo  11634  fsumparts  11638  hashiun  11646  binomlem  11651  binom1dif  11655  bcxmas  11657  isumsplit  11659  isum1p  11660  arisum  11666  arisum2  11667  trireciplem  11668  explecnv  11673  geolim  11679  georeclim  11681  mertenslem2  11704  mertensabs  11705  prodf1f  11711  prodrbdclem2  11741  efcllemp  11826  ef0lem  11828  efgt0  11852  eftlub  11858  efsep  11859  effsumlt  11860  tanval3ap  11882  efi4p  11885  resin4p  11886  recos4p  11887  ef01bndlem  11924  sin01bnd  11925  cos01bnd  11926  sinltxirr  11929  sin01gt0  11930  cos01gt0  11931  absefib  11939  efieq1re  11940  eirraplem  11945  dvdsdc  11966  dvdscmulr  11988  fsumdvds  12010  dvdslelemd  12011  3dvds  12032  odd2np1lem  12040  odd2np1  12041  flodddiv4  12104  bitsfzo  12123  bitsmod  12124  gcdsupex  12135  gcdsupcl  12136  gcd1  12165  nninfctlemfo  12218  nn0seqcvgd  12220  algcvg  12227  algcvgblem  12228  eucalg  12238  prmind2  12299  qden1elz  12384  dfphi2  12399  phiprm  12402  phimullem  12404  prmdiv  12414  prmdiveq  12415  prm23lt5  12443  pcpre1  12472  pczpre  12477  pcdiv  12482  pc1  12485  pcqdiv  12487  pcexp  12489  pcxnn0cl  12490  pcxcl  12491  pcdvdstr  12507  pc2dvds  12510  sumhashdc  12527  fldivp1  12528  pcfaclem  12529  qexpz  12532  expnprm  12533  prmpwdvds  12535  pockthlem  12536  4sqlem5  12562  4sqlem6  12563  4sqlem11  12581  4sqlem13m  12583  4sqlem19  12589  oddennn  12620  xpct  12624  ennnfonelemj0  12629  ennnfonelemen  12649  ctinfomlemom  12655  omctfn  12671  restid  12938  prdsex  12957  prdsval  12961  prdsbaslemss  12962  prdsbas  12964  imasbas  12976  imasplusg  12977  imasmulr  12978  imasaddfnlemg  12983  xpscf  13016  igsumvalx  13058  gsumsplit1r  13067  gsumprval  13068  gsumfzz  13153  gsumfzcl  13157  mulgnngsum  13283  mulgnndir  13307  mulgneg2  13312  dvdsrmuld  13678  zsssubrg  14167  znval  14218  znle  14219  znbaslemnn  14221  znf1o  14233  znleval  14235  psrval  14246  restuni2  14439  cnrest2r  14499  lmfss  14506  lmres  14510  lmtopcnp  14512  ispsmet  14585  isxmet2d  14610  ismet2  14616  blfvalps  14647  blex  14649  xblss2  14667  reopnap  14808  divcnap  14827  climcncf  14846  cncfmpt2fcntop  14861  hovera  14909  limcdifap  14924  cnplimcim  14929  cnlimcim  14933  cnlimc  14934  cnlimci  14935  dvbss  14947  dvcnp2cntop  14961  dvcn  14962  dvaddxxbr  14963  dvmulxxbr  14964  dvexp  14973  dveflem  14988  plyval  14994  elply2  14997  plyf  14999  plyss  15000  plyssc  15001  elplyr  15002  plyaddlem1  15009  plymullem1  15010  plyaddlem  15011  plymullem  15012  plyco  15021  plycj  15023  dvply1  15027  reeff1olem  15033  sinperlem  15070  sin2kpi  15073  cos2kpi  15074  sin2pim  15075  cos2pim  15076  cosq14gt0  15094  coseq0q4123  15096  tangtx  15100  abssinper  15108  sinkpi  15109  coskpi  15110  cosq34lt1  15112  logrpap0b  15138  logdivlti  15143  rpcxpsqrtth  15192  rpabscxpbnd  15202  binom4  15241  wilthlem1  15242  0sgm  15247  1sgmprm  15256  1sgm2ppw  15257  mersenne  15259  perfect1  15260  perfectlem1  15261  perfectlem2  15262  perfect  15263  lgslem1  15267  lgsval  15271  lgsfvalg  15272  lgsfcl2  15273  lgsfcl  15275  lgsval2lem  15277  lgsvalmod  15286  lgsneg  15291  lgsdilem  15294  lgsdir2lem3  15297  lgsdir  15302  lgsdilem2  15303  lgsdi  15304  lgsne0  15305  lgsabs1  15306  lgsprme0  15309  lgsdirnn0  15314  lgsdinn0  15315  gausslemma2dlem0d  15319  gausslemma2dlem1a  15325  gausslemma2dlem1f1o  15327  gausslemma2dlem3  15330  gausslemma2dlem4  15331  gausslemma2dlem5a  15332  gausslemma2dlem5  15333  gausslemma2dlem6  15334  lgseisenlem2  15338  lgseisen  15341  lgsquadlem1  15344  lgsquadlem2  15345  lgsquad2lem1  15348  lgsquad2lem2  15349  lgsquad2  15350  m1lgs  15352  2lgslem1  15358  2lgslem2  15359  2lgs  15371  2sqlem9  15391  2sqlem10  15392  2omap  15668  pwle2  15671  pw1nct  15676  nninfsellemdc  15683  nnnninfen  15694  sbthom  15699  trirec0  15717  apdifflemr  15720  reap0  15731  nconstwlpolem  15738