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  1759  sseqtrid  3207  ssdifin0  3506  uneqdifeqim  3510  unimax  3845  opth  4239  djussxp  4774  iss  4955  relresfld  5160  eldmrexrn  5659  f1oresrab  5683  fmptco  5684  fsn  5690  fnressn  5704  foima2  5754  foeqcnvco  5793  isoini2  5822  ofres  6099  ofco  6103  tposexg  6261  tfrlemisucaccv  6328  tfrlemibex  6332  tfri1dALT  6354  tfrcl  6367  rdgivallem  6384  frecabex  6401  frectfr  6403  frecrdg  6411  pmresg  6678  mapsn  6692  mapsncnv  6697  ixpsnf1o  6738  en1  6801  2dom  6807  enpr2d  6819  mapxpen  6850  phplem4  6857  fiintim  6930  sbthlem2  6959  elfir  6974  infglbti  7026  caseinl  7092  caseinr  7093  difinfsnlem  7100  difinfsn  7101  nninfisollemne  7131  exmidfodomrlemim  7202  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  2omotaplemap  7258  archnqq  7418  prarloclemlt  7494  prarloclemlo  7495  prarloclemcalc  7503  recexprlemm  7625  recexprlemex  7638  caucvgprlemm  7669  caucvgprprlemmu  7696  suplocexprlem2b  7715  suplocexprlemmu  7719  suplocexprlemlub  7725  1idsr  7769  recexgt0sr  7774  archsr  7783  caucvgsrlemoffval  7797  caucvgsrlemofff  7798  caucvgsrlemoffres  7801  caucvgsr  7803  ltpsrprg  7804  suplocsrlem  7809  pitonnlem2  7848  pitonn  7849  pitoregt0  7850  pitore  7851  recnnre  7852  axrnegex  7880  nntopi  7895  msqge0  8575  mulge0  8578  recexaplem2  8611  recexap  8612  recgt0  8809  recreclt  8859  nn1m1nn  8939  nn1suc  8940  nnle1eq1  8945  nn1gt1  8955  nnsub  8960  addltmul  9157  nn0le0eq0  9206  elnn0nn  9220  elnnz  9265  elznn0  9270  zlem1lt  9311  zltlem1  9312  elz2  9326  nn0n0n1ge2b  9334  nn0lt2  9336  nn0le2is012  9337  eluzaddi  9556  eluzsubi  9557  uzp1  9563  peano2uzr  9587  nn01to3  9619  qreccl  9644  ltpnf  9782  xaddass2  9872  iccen  10008  fz01en  10055  fzpreddisj  10073  fzsuc2  10081  fseq1p1m1  10096  fseq1m1p1  10097  elfzp1b  10099  fzoss2  10174  fzval3  10206  fzosplitsnm1  10211  fzosplitprm1  10236  flhalf  10304  modqmulnn  10344  modqmuladdnn0  10370  frec2uzrand  10407  frecuzrdg0  10415  frecuzrdg0t  10424  frecfzennn  10428  frecfzen2  10429  uzennn  10438  seqeq1  10450  seq3m1  10470  monoord2  10479  ser3mono  10480  ser0f  10517  exp3vallem  10523  expm1t  10550  expeq0  10553  expubnd  10579  binom3  10640  facndiv  10721  facavg  10728  bcn0  10737  bcnp1n  10741  bcm1k  10742  bcp1nk  10744  bcval5  10745  bcn2  10746  bcp1m1  10747  bcpasc  10748  bcn2m1  10751  hashsng  10780  hashun  10787  hashfz  10803  hashfzo  10804  seq3coll  10824  shftfval  10832  2shfti  10842  resqrexlemf1  11019  abs00ap  11073  sqabs  11093  ltabs  11098  caubnd2  11128  max0addsup  11230  rexico  11232  mulcn2  11322  climaddc1  11339  climmulc2  11341  climsubc1  11342  climsubc2  11343  iserex  11349  climlec2  11351  iser3shft  11356  climcvg1nlem  11359  serf0  11362  sumrbdc  11389  fsumm1  11426  fsump1  11430  fsum00  11472  telfsumo  11476  fsumparts  11480  hashiun  11488  binomlem  11493  binom1dif  11497  bcxmas  11499  isumsplit  11501  isum1p  11502  arisum  11508  arisum2  11509  trireciplem  11510  explecnv  11515  geolim  11521  georeclim  11523  mertenslem2  11546  mertensabs  11547  prodf1f  11553  prodrbdclem2  11583  efcllemp  11668  ef0lem  11670  efgt0  11694  eftlub  11700  efsep  11701  effsumlt  11702  tanval3ap  11724  efi4p  11727  resin4p  11728  recos4p  11729  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  cos01gt0  11772  absefib  11780  efieq1re  11781  eirraplem  11786  dvdsdc  11807  dvdscmulr  11829  dvdslelemd  11851  odd2np1lem  11879  odd2np1  11880  flodddiv4  11941  gcdsupex  11960  gcdsupcl  11961  gcd1  11990  nn0seqcvgd  12043  algcvg  12050  algcvgblem  12051  eucalg  12061  prmind2  12122  qden1elz  12207  dfphi2  12222  phiprm  12225  phimullem  12227  prmdiv  12237  prmdiveq  12238  prm23lt5  12265  pcpre1  12294  pczpre  12299  pcdiv  12304  pc1  12307  pcqdiv  12309  pcexp  12311  pcxnn0cl  12312  pcxcl  12313  pcdvdstr  12328  pc2dvds  12331  sumhashdc  12347  fldivp1  12348  pcfaclem  12349  qexpz  12352  expnprm  12353  prmpwdvds  12355  pockthlem  12356  4sqlem5  12382  4sqlem6  12383  oddennn  12395  xpct  12399  ennnfonelemj0  12404  ennnfonelemen  12424  ctinfomlemom  12430  omctfn  12446  restid  12704  prdsex  12723  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfnlemg  12740  xpscf  12771  mulgnndir  13017  mulgneg2  13022  dvdsrmuld  13270  zsssubrg  13564  restuni2  13762  cnrest2r  13822  lmfss  13829  lmres  13833  lmtopcnp  13835  ispsmet  13908  isxmet2d  13933  ismet2  13939  blfvalps  13970  blex  13972  xblss2  13990  reopnap  14123  divcnap  14140  climcncf  14156  cncfmpt2fcntop  14170  limcdifap  14216  cnplimcim  14221  cnlimcim  14225  cnlimc  14226  cnlimci  14227  dvbss  14239  dvcnp2cntop  14248  dvcn  14249  dvaddxxbr  14250  dvmulxxbr  14251  dvexp  14260  dveflem  14272  reeff1olem  14277  sinperlem  14314  sin2kpi  14317  cos2kpi  14318  sin2pim  14319  cos2pim  14320  cosq14gt0  14338  coseq0q4123  14340  tangtx  14344  abssinper  14352  sinkpi  14353  coskpi  14354  cosq34lt1  14356  logrpap0b  14382  logdivlti  14387  rpcxpsqrtth  14435  rpabscxpbnd  14444  binom4  14482  lgslem1  14486  lgsval  14490  lgsfvalg  14491  lgsfcl2  14492  lgsfcl  14494  lgsval2lem  14496  lgsvalmod  14505  lgsneg  14510  lgsdilem  14513  lgsdir2lem3  14516  lgsdir  14521  lgsdilem2  14522  lgsdi  14523  lgsne0  14524  lgsabs1  14525  lgsprme0  14528  lgsdirnn0  14533  lgsdinn0  14534  lgseisenlem2  14536  m1lgs  14537  2sqlem9  14556  2sqlem10  14557  pwle2  14833  pw1nct  14837  nninfsellemdc  14844  sbthom  14859  trirec0  14877  apdifflemr  14880  reap0  14891  nconstwlpolem  14898