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  5706  f1oresrab  5730  fmptco  5731  fsn  5737  fnressn  5751  foima2  5801  foeqcnvco  5840  isoini2  5869  ofres  6154  ofco  6158  tposexg  6325  tfrlemisucaccv  6392  tfrlemibex  6396  tfri1dALT  6418  tfrcl  6431  rdgivallem  6448  frecabex  6465  frectfr  6467  frecrdg  6475  pmresg  6744  mapsn  6758  mapsncnv  6763  ixpsnf1o  6804  en1  6867  2dom  6873  enpr2d  6885  mapxpen  6918  phplem4  6925  exmidpw2en  6982  fiintim  7001  sbthlem2  7033  elfir  7048  infglbti  7100  caseinl  7166  caseinr  7167  difinfsnlem  7174  difinfsn  7175  nninfisollemne  7206  exmidfodomrlemim  7280  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  2omotaplemap  7340  archnqq  7501  prarloclemlt  7577  prarloclemlo  7578  prarloclemcalc  7586  recexprlemm  7708  recexprlemex  7721  caucvgprlemm  7752  caucvgprprlemmu  7779  suplocexprlem2b  7798  suplocexprlemmu  7802  suplocexprlemlub  7808  1idsr  7852  recexgt0sr  7857  archsr  7866  caucvgsrlemoffval  7880  caucvgsrlemofff  7881  caucvgsrlemoffres  7884  caucvgsr  7886  ltpsrprg  7887  suplocsrlem  7892  pitonnlem2  7931  pitonn  7932  pitoregt0  7933  pitore  7934  recnnre  7935  axrnegex  7963  nntopi  7978  msqge0  8660  mulge0  8663  recexaplem2  8696  recexap  8697  recgt0  8894  recreclt  8944  nn1m1nn  9025  nn1suc  9026  nnle1eq1  9031  nn1gt1  9041  nnsub  9046  addltmul  9245  nn0le0eq0  9294  elnn0nn  9308  elnnz  9353  elznn0  9358  zlem1lt  9399  zltlem1  9400  elz2  9414  nn0n0n1ge2b  9422  nn0lt2  9424  nn0le2is012  9425  eluzaddi  9645  eluzsubi  9646  uzp1  9652  peano2uzr  9676  nn01to3  9708  qreccl  9733  irrmulap  9739  ltpnf  9872  xaddass2  9962  iccen  10098  fz01en  10145  fzpreddisj  10163  fzsuc2  10171  fseq1p1m1  10186  fseq1m1p1  10187  elfzp1b  10189  fzoss2  10265  fzval3  10297  fzosplitsnm1  10302  fzosplitprm1  10327  flhalf  10409  fldiv4lem1div2uz2  10413  modqmulnn  10451  modqmuladdnn0  10477  frec2uzrand  10514  frecuzrdg0  10522  frecuzrdg0t  10531  frecfzennn  10535  frecfzen2  10536  uzennn  10545  seqeq1  10559  seqp1g  10575  seqclg  10581  seq3m1  10582  monoord2  10595  ser3mono  10596  seqf1oglem1  10628  seqf1oglem2  10629  seqfeq4g  10640  ser0f  10643  exp3vallem  10649  expm1t  10676  expeq0  10679  expubnd  10705  binom3  10766  facndiv  10848  facavg  10855  bcn0  10864  bcnp1n  10868  bcm1k  10869  bcp1nk  10871  bcval5  10872  bcn2  10873  bcp1m1  10874  bcpasc  10875  bcn2m1  10878  hashsng  10907  hashun  10914  hashfz  10930  hashfzo  10931  seq3coll  10951  iswrdiz  10959  snopiswrd  10962  shftfval  11003  2shfti  11013  resqrexlemf1  11190  abs00ap  11244  sqabs  11264  ltabs  11269  caubnd2  11299  max0addsup  11401  rexico  11403  mulcn2  11494  climaddc1  11511  climmulc2  11513  climsubc1  11514  climsubc2  11515  iserex  11521  climlec2  11523  iser3shft  11528  climcvg1nlem  11531  serf0  11534  sumrbdc  11561  fsumm1  11598  fsump1  11602  fsum00  11644  telfsumo  11648  fsumparts  11652  hashiun  11660  binomlem  11665  binom1dif  11669  bcxmas  11671  isumsplit  11673  isum1p  11674  arisum  11680  arisum2  11681  trireciplem  11682  explecnv  11687  geolim  11693  georeclim  11695  mertenslem2  11718  mertensabs  11719  prodf1f  11725  prodrbdclem2  11755  efcllemp  11840  ef0lem  11842  efgt0  11866  eftlub  11872  efsep  11873  effsumlt  11874  tanval3ap  11896  efi4p  11899  resin4p  11900  recos4p  11901  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  sinltxirr  11943  sin01gt0  11944  cos01gt0  11945  absefib  11953  efieq1re  11954  eirraplem  11959  dvdsdc  11980  dvdscmulr  12002  fsumdvds  12024  dvdslelemd  12025  3dvds  12046  odd2np1lem  12054  odd2np1  12055  flodddiv4  12118  bitsfzo  12137  bitsmod  12138  gcdsupex  12149  gcdsupcl  12150  gcd1  12179  nninfctlemfo  12232  nn0seqcvgd  12234  algcvg  12241  algcvgblem  12242  eucalg  12252  prmind2  12313  qden1elz  12398  dfphi2  12413  phiprm  12416  phimullem  12418  prmdiv  12428  prmdiveq  12429  prm23lt5  12457  pcpre1  12486  pczpre  12491  pcdiv  12496  pc1  12499  pcqdiv  12501  pcexp  12503  pcxnn0cl  12504  pcxcl  12505  pcdvdstr  12521  pc2dvds  12524  sumhashdc  12541  fldivp1  12542  pcfaclem  12543  qexpz  12546  expnprm  12547  prmpwdvds  12549  pockthlem  12550  4sqlem5  12576  4sqlem6  12577  4sqlem11  12595  4sqlem13m  12597  4sqlem19  12603  oddennn  12634  xpct  12638  ennnfonelemj0  12643  ennnfonelemen  12663  ctinfomlemom  12669  omctfn  12685  restid  12952  prdsex  12971  prdsval  12975  prdsbaslemss  12976  prdsbas  12978  imasbas  13009  imasplusg  13010  imasmulr  13011  imasaddfnlemg  13016  xpscf  13049  igsumvalx  13091  gsumsplit1r  13100  gsumprval  13101  gsumfzz  13197  gsumfzcl  13201  prdsgrpd  13311  prdsinvgd  13312  mulgnngsum  13333  mulgnndir  13357  mulgneg2  13362  dvdsrmuld  13728  zsssubrg  14217  znval  14268  znle  14269  znbaslemnn  14271  znf1o  14283  znleval  14285  psrval  14296  restuni2  14497  cnrest2r  14557  lmfss  14564  lmres  14568  lmtopcnp  14570  ispsmet  14643  isxmet2d  14668  ismet2  14674  blfvalps  14705  blex  14707  xblss2  14725  reopnap  14866  divcnap  14885  climcncf  14904  cncfmpt2fcntop  14919  hovera  14967  limcdifap  14982  cnplimcim  14987  cnlimcim  14991  cnlimc  14992  cnlimci  14993  dvbss  15005  dvcnp2cntop  15019  dvcn  15020  dvaddxxbr  15021  dvmulxxbr  15022  dvexp  15031  dveflem  15046  plyval  15052  elply2  15055  plyf  15057  plyss  15058  plyssc  15059  elplyr  15060  plyaddlem1  15067  plymullem1  15068  plyaddlem  15069  plymullem  15070  plyco  15079  plycj  15081  dvply1  15085  reeff1olem  15091  sinperlem  15128  sin2kpi  15131  cos2kpi  15132  sin2pim  15133  cos2pim  15134  cosq14gt0  15152  coseq0q4123  15154  tangtx  15158  abssinper  15166  sinkpi  15167  coskpi  15168  cosq34lt1  15170  logrpap0b  15196  logdivlti  15201  rpcxpsqrtth  15250  rpabscxpbnd  15260  binom4  15299  wilthlem1  15300  0sgm  15305  1sgmprm  15314  1sgm2ppw  15315  mersenne  15317  perfect1  15318  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgslem1  15325  lgsval  15329  lgsfvalg  15330  lgsfcl2  15331  lgsfcl  15333  lgsval2lem  15335  lgsvalmod  15344  lgsneg  15349  lgsdilem  15352  lgsdir2lem3  15355  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgsabs1  15364  lgsprme0  15367  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem0d  15377  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem3  15388  gausslemma2dlem4  15389  gausslemma2dlem5a  15390  gausslemma2dlem5  15391  gausslemma2dlem6  15392  lgseisenlem2  15396  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem1  15406  lgsquad2lem2  15407  lgsquad2  15408  m1lgs  15410  2lgslem1  15416  2lgslem2  15417  2lgs  15429  2sqlem9  15449  2sqlem10  15450  2omap  15726  pwle2  15729  pw1nct  15734  nninfsellemdc  15741  nnnninfen  15752  sbthom  15757  trirec0  15775  apdifflemr  15778  reap0  15789  nconstwlpolem  15796