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  1770  sseqtrid  3220  ssdifin0  3519  uneqdifeqim  3523  unimax  3858  opth  4255  djussxp  4790  iss  4971  relresfld  5176  eldmrexrn  5677  f1oresrab  5701  fmptco  5702  fsn  5708  fnressn  5722  foima2  5772  foeqcnvco  5811  isoini2  5840  ofres  6120  ofco  6124  tposexg  6282  tfrlemisucaccv  6349  tfrlemibex  6353  tfri1dALT  6375  tfrcl  6388  rdgivallem  6405  frecabex  6422  frectfr  6424  frecrdg  6432  pmresg  6701  mapsn  6715  mapsncnv  6720  ixpsnf1o  6761  en1  6824  2dom  6830  enpr2d  6842  mapxpen  6875  phplem4  6882  exmidpw2en  6939  fiintim  6956  sbthlem2  6986  elfir  7001  infglbti  7053  caseinl  7119  caseinr  7120  difinfsnlem  7127  difinfsn  7128  nninfisollemne  7158  exmidfodomrlemim  7229  exmidfodomrlemr  7230  exmidfodomrlemrALT  7231  2omotaplemap  7285  archnqq  7445  prarloclemlt  7521  prarloclemlo  7522  prarloclemcalc  7530  recexprlemm  7652  recexprlemex  7665  caucvgprlemm  7696  caucvgprprlemmu  7723  suplocexprlem2b  7742  suplocexprlemmu  7746  suplocexprlemlub  7752  1idsr  7796  recexgt0sr  7801  archsr  7810  caucvgsrlemoffval  7824  caucvgsrlemofff  7825  caucvgsrlemoffres  7828  caucvgsr  7830  ltpsrprg  7831  suplocsrlem  7836  pitonnlem2  7875  pitonn  7876  pitoregt0  7877  pitore  7878  recnnre  7879  axrnegex  7907  nntopi  7922  msqge0  8602  mulge0  8605  recexaplem2  8638  recexap  8639  recgt0  8836  recreclt  8886  nn1m1nn  8966  nn1suc  8967  nnle1eq1  8972  nn1gt1  8982  nnsub  8987  addltmul  9184  nn0le0eq0  9233  elnn0nn  9247  elnnz  9292  elznn0  9297  zlem1lt  9338  zltlem1  9339  elz2  9353  nn0n0n1ge2b  9361  nn0lt2  9363  nn0le2is012  9364  eluzaddi  9583  eluzsubi  9584  uzp1  9590  peano2uzr  9614  nn01to3  9646  qreccl  9671  ltpnf  9809  xaddass2  9899  iccen  10035  fz01en  10082  fzpreddisj  10100  fzsuc2  10108  fseq1p1m1  10123  fseq1m1p1  10124  elfzp1b  10126  fzoss2  10201  fzval3  10233  fzosplitsnm1  10238  fzosplitprm1  10263  flhalf  10332  modqmulnn  10372  modqmuladdnn0  10398  frec2uzrand  10435  frecuzrdg0  10443  frecuzrdg0t  10452  frecfzennn  10456  frecfzen2  10457  uzennn  10466  seqeq1  10478  seq3m1  10498  monoord2  10507  ser3mono  10508  ser0f  10545  exp3vallem  10551  expm1t  10578  expeq0  10581  expubnd  10607  binom3  10668  facndiv  10750  facavg  10757  bcn0  10766  bcnp1n  10770  bcm1k  10771  bcp1nk  10773  bcval5  10774  bcn2  10775  bcp1m1  10776  bcpasc  10777  bcn2m1  10780  hashsng  10809  hashun  10816  hashfz  10832  hashfzo  10833  seq3coll  10853  shftfval  10861  2shfti  10871  resqrexlemf1  11048  abs00ap  11102  sqabs  11122  ltabs  11127  caubnd2  11157  max0addsup  11259  rexico  11261  mulcn2  11351  climaddc1  11368  climmulc2  11370  climsubc1  11371  climsubc2  11372  iserex  11378  climlec2  11380  iser3shft  11385  climcvg1nlem  11388  serf0  11391  sumrbdc  11418  fsumm1  11455  fsump1  11459  fsum00  11501  telfsumo  11505  fsumparts  11509  hashiun  11517  binomlem  11522  binom1dif  11526  bcxmas  11528  isumsplit  11530  isum1p  11531  arisum  11537  arisum2  11538  trireciplem  11539  explecnv  11544  geolim  11550  georeclim  11552  mertenslem2  11575  mertensabs  11576  prodf1f  11582  prodrbdclem2  11612  efcllemp  11697  ef0lem  11699  efgt0  11723  eftlub  11729  efsep  11730  effsumlt  11731  tanval3ap  11753  efi4p  11756  resin4p  11757  recos4p  11758  ef01bndlem  11795  sin01bnd  11796  cos01bnd  11797  sin01gt0  11800  cos01gt0  11801  absefib  11809  efieq1re  11810  eirraplem  11815  dvdsdc  11836  dvdscmulr  11858  dvdslelemd  11880  odd2np1lem  11908  odd2np1  11909  flodddiv4  11970  gcdsupex  11989  gcdsupcl  11990  gcd1  12019  nn0seqcvgd  12072  algcvg  12079  algcvgblem  12080  eucalg  12090  prmind2  12151  qden1elz  12236  dfphi2  12251  phiprm  12254  phimullem  12256  prmdiv  12266  prmdiveq  12267  prm23lt5  12294  pcpre1  12323  pczpre  12328  pcdiv  12333  pc1  12336  pcqdiv  12338  pcexp  12340  pcxnn0cl  12341  pcxcl  12342  pcdvdstr  12358  pc2dvds  12361  sumhashdc  12378  fldivp1  12379  pcfaclem  12380  qexpz  12383  expnprm  12384  prmpwdvds  12386  pockthlem  12387  4sqlem5  12413  4sqlem6  12414  4sqlem11  12432  4sqlem13m  12434  4sqlem19  12440  oddennn  12442  xpct  12446  ennnfonelemj0  12451  ennnfonelemen  12471  ctinfomlemom  12477  omctfn  12493  restid  12752  prdsex  12771  imasbas  12781  imasplusg  12782  imasmulr  12783  imasaddfnlemg  12788  xpscf  12820  mulgnndir  13088  mulgneg2  13093  dvdsrmuld  13443  zsssubrg  13885  znval  13929  znle  13930  znbaslemnn  13932  psrval  13941  psrex  13942  restuni2  14129  cnrest2r  14189  lmfss  14196  lmres  14200  lmtopcnp  14202  ispsmet  14275  isxmet2d  14300  ismet2  14306  blfvalps  14337  blex  14339  xblss2  14357  reopnap  14490  divcnap  14507  climcncf  14523  cncfmpt2fcntop  14537  limcdifap  14583  cnplimcim  14588  cnlimcim  14592  cnlimc  14593  cnlimci  14594  dvbss  14606  dvcnp2cntop  14615  dvcn  14616  dvaddxxbr  14617  dvmulxxbr  14618  dvexp  14627  dveflem  14639  reeff1olem  14644  sinperlem  14681  sin2kpi  14684  cos2kpi  14685  sin2pim  14686  cos2pim  14687  cosq14gt0  14705  coseq0q4123  14707  tangtx  14711  abssinper  14719  sinkpi  14720  coskpi  14721  cosq34lt1  14723  logrpap0b  14749  logdivlti  14754  rpcxpsqrtth  14802  rpabscxpbnd  14811  binom4  14849  wilthlem1  14850  lgslem1  14854  lgsval  14858  lgsfvalg  14859  lgsfcl2  14860  lgsfcl  14862  lgsval2lem  14864  lgsvalmod  14873  lgsneg  14878  lgsdilem  14881  lgsdir2lem3  14884  lgsdir  14889  lgsdilem2  14890  lgsdi  14891  lgsne0  14892  lgsabs1  14893  lgsprme0  14896  lgsdirnn0  14901  lgsdinn0  14902  lgseisenlem2  14904  m1lgs  14905  2sqlem9  14924  2sqlem10  14925  pwle2  15202  pw1nct  15206  nninfsellemdc  15213  sbthom  15228  trirec0  15246  apdifflemr  15249  reap0  15260  nconstwlpolem  15267