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  1808  sseqtrid  3292  ssdifin0  3595  uneqdifeqim  3599  unimax  3953  opth  4358  djussxp  4905  iss  5089  relresfld  5297  eldmrexrn  5823  f1oresrab  5847  fmptco  5848  fsn  5854  fnressn  5875  foima2  5930  foeqcnvco  5969  isoini2  5998  relmptopab  6264  ofres  6290  ofco  6294  suppval1  6452  suppimacnvfn  6459  tposexg  6502  tfrlemisucaccv  6569  tfrlemibex  6573  tfri1dALT  6595  tfrcl  6608  rdgivallem  6625  frecabex  6642  frectfr  6644  frecrdg  6652  pmresg  6923  mapsnd  6936  mapsn  6938  mapsncnv  6943  ixpsnf1o  6984  en1  7052  2dom  7059  mapsnend  7065  enpr2d  7077  en2  7078  mapxpen  7114  mapunen  7117  phplem4  7122  exmidpw2en  7185  fiintim  7204  sbthlem2  7241  elfir  7273  2omap  7282  infglbti  7329  caseinl  7395  caseinr  7396  difinfsnlem  7403  difinfsn  7404  nninfisollemne  7435  exmidfodomrlemim  7517  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  2omotaplemap  7587  archnqq  7748  prarloclemlt  7824  prarloclemlo  7825  prarloclemcalc  7833  recexprlemm  7955  recexprlemex  7968  caucvgprlemm  7999  caucvgprprlemmu  8026  suplocexprlem2b  8045  suplocexprlemmu  8049  suplocexprlemlub  8055  1idsr  8099  recexgt0sr  8104  archsr  8113  caucvgsrlemoffval  8127  caucvgsrlemofff  8128  caucvgsrlemoffres  8131  caucvgsr  8133  ltpsrprg  8134  suplocsrlem  8139  pitonnlem2  8178  pitonn  8179  pitoregt0  8180  pitore  8181  recnnre  8182  axrnegex  8210  nntopi  8225  msqge0  8908  mulge0  8911  recexaplem2  8944  recexap  8945  recgt0  9144  recreclt  9194  nn1m1nn  9275  nn1suc  9276  nnle1eq1  9281  nn1gt1  9291  nnsub  9296  addltmul  9495  nn0le0eq0  9544  elnn0nn  9558  elnnz  9607  elznn0  9612  zlem1lt  9654  zltlem1  9655  elz2  9669  nn0n0n1ge2b  9678  nn0lt2  9680  nn0le2is012  9681  eluzaddi  9902  eluzsubi  9903  uzp1  9909  peano2uzr  9938  nn01to3  9970  qreccl  9995  irrmulap  10001  ltpnf  10135  xaddass2  10225  iccen  10362  fz01en  10411  fzpreddisj  10430  fzsuc2  10438  fseq1p1m1  10453  fseq1m1p1  10454  elfzp1b  10456  fzoss2  10533  fzval3  10574  fzosplitsnm1  10579  fzosplitprm1  10605  flhalf  10689  fldiv4lem1div2uz2  10693  modqmulnn  10731  modqmuladdnn0  10757  frec2uzrand  10794  frecuzrdg0  10802  frecuzrdg0t  10811  frecfzennn  10815  frecfzen2  10816  uzennn  10825  seqeq1  10839  seqp1g  10855  seqclg  10861  seq3m1  10862  monoord2  10875  ser3mono  10876  seqf1oglem1  10908  seqf1oglem2  10909  seqfeq4g  10920  ser0f  10923  exp3vallem  10929  expm1t  10956  expeq0  10959  expubnd  10985  binom3  11046  facndiv  11129  facavg  11136  bcn0  11145  bcnp1n  11149  bcm1k  11150  bcp1nk  11152  bcval5  11153  bcn2  11154  bcp1m1  11155  bcpasc  11156  bcn2m1  11160  hashsng  11189  hashun  11197  hashfz  11214  hashfzo  11215  hashmap  11220  hashfibclem  11234  seq3coll  11242  hash2en  11243  iswrdiz  11259  snopiswrd  11262  ccat1st1st  11357  swrds1  11388  cats1un  11441  wrdind  11442  wrd2ind  11443  swrdccatin1  11445  swrdccat3blem  11459  shftfval  11534  2shfti  11544  resqrexlemf1  11722  abs00ap  11776  sqabs  11796  ltabs  11801  caubnd2  11831  max0addsup  11933  rexico  11935  mulcn2  12026  climaddc1  12043  climmulc2  12045  climsubc1  12046  climsubc2  12047  iserex  12053  climlec2  12055  iser3shft  12060  climcvg1nlem  12063  serf0  12066  sumrbdc  12094  fsumm1  12131  fsump1  12135  fsum00  12177  telfsumo  12181  fsumparts  12185  hashiun  12193  binomlem  12198  binom1dif  12202  bcxmas  12204  isumsplit  12206  isum1p  12207  arisum  12213  arisum2  12214  trireciplem  12215  explecnv  12220  geolim  12226  georeclim  12228  mertenslem2  12251  mertensabs  12252  prodf1f  12258  prodrbdclem2  12288  efcllemp  12373  ef0lem  12375  efgt0  12399  eftlub  12405  efsep  12406  effsumlt  12407  tanval3ap  12429  efi4p  12432  resin4p  12433  recos4p  12434  ef01bndlem  12471  sin01bnd  12472  cos01bnd  12473  sinltxirr  12476  sin01gt0  12477  cos01gt0  12478  absefib  12486  efieq1re  12487  eirraplem  12492  dvdsdc  12513  dvdscmulr  12535  fsumdvds  12557  dvdslelemd  12558  3dvds  12579  odd2np1lem  12587  odd2np1  12588  flodddiv4  12651  bitsfzo  12670  bitsmod  12671  gcdsupex  12682  gcdsupcl  12683  gcd1  12712  nninfctlemfo  12765  nn0seqcvgd  12767  algcvg  12774  algcvgblem  12775  eucalg  12785  prmind2  12846  qden1elz  12931  dfphi2  12946  phiprm  12949  phimullem  12951  prmdiv  12961  prmdiveq  12962  prm23lt5  12990  pcpre1  13019  pczpre  13024  pcdiv  13029  pc1  13032  pcqdiv  13034  pcexp  13036  pcxnn0cl  13037  pcxcl  13038  pcdvdstr  13054  pc2dvds  13057  sumhashdc  13074  fldivp1  13075  pcfaclem  13076  qexpz  13079  expnprm  13080  prmpwdvds  13082  pockthlem  13083  4sqlem5  13109  4sqlem6  13110  4sqlem11  13128  4sqlem13m  13130  4sqlem19  13136  ballotfilemofi  13167  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemodife  13188  ballotfilemscl  13195  ballotfilemsle  13196  oddennn  13231  xpct  13235  ennnfonelemj0  13240  ennnfonelemen  13260  ctinfomlemom  13266  omctfn  13282  restid  13551  imasbas  13575  imasplusg  13576  imasmulr  13577  imasaddfnlemg  13582  xpscf  13615  igsumvalx  13656  gsumsplit1r  13665  gsumprval  13666  gsumfzz  13754  gsumfzcl  13758  mulgnngsum  13884  mulgnndir  13908  mulgneg2  13913  gfsumval  14106  prdsex  14118  prdsval  14119  prdsbaslemss  14120  prdsbas  14122  prdsgrpd  14143  prdsinvgd  14144  dvdsrmuld  14345  zsssubrg  14863  znval  14914  znle  14915  znbaslemnn  14917  znf1o  14929  znleval  14931  psrval  14944  restuni2  15172  cnrest2r  15232  lmfss  15239  lmres  15243  lmtopcnp  15245  ispsmet  15318  isxmet2d  15343  ismet2  15349  blfvalps  15380  blex  15382  xblss2  15400  reopnap  15541  divcnap  15560  climcncf  15579  cncfmpt2fcntop  15594  hovera  15642  limcdifap  15657  cnplimcim  15662  cnlimcim  15666  cnlimc  15667  cnlimci  15668  dvbss  15680  dvcnp2cntop  15694  dvcn  15695  dvaddxxbr  15696  dvmulxxbr  15697  dvexp  15706  dveflem  15721  plyval  15727  elply2  15730  plyf  15732  plyss  15733  plyssc  15734  elplyr  15735  plyaddlem1  15742  plymullem1  15743  plyaddlem  15744  plymullem  15745  plyco  15754  plycj  15756  dvply1  15760  reeff1olem  15766  sinperlem  15803  sin2kpi  15806  cos2kpi  15807  sin2pim  15808  cos2pim  15809  cosq14gt0  15827  coseq0q4123  15829  tangtx  15833  abssinper  15841  sinkpi  15842  coskpi  15843  cosq34lt1  15845  logrpap0b  15871  logdivlti  15876  rpcxpsqrtth  15925  rpabscxpbnd  15935  binom4  15974  wilthlem1  15978  0sgm  15983  1sgmprm  15992  1sgm2ppw  15993  mersenne  15995  perfect1  15996  perfectlem1  15997  perfectlem2  15998  perfect  15999  lgslem1  16003  lgsval  16007  lgsfvalg  16008  lgsfcl2  16009  lgsfcl  16011  lgsval2lem  16013  lgsvalmod  16022  lgsneg  16027  lgsdilem  16030  lgsdir2lem3  16033  lgsdir  16038  lgsdilem2  16039  lgsdi  16040  lgsne0  16041  lgsabs1  16042  lgsprme0  16045  lgsdirnn0  16050  lgsdinn0  16051  gausslemma2dlem0d  16055  gausslemma2dlem1a  16061  gausslemma2dlem1f1o  16063  gausslemma2dlem3  16066  gausslemma2dlem4  16067  gausslemma2dlem5a  16068  gausslemma2dlem5  16069  gausslemma2dlem6  16070  lgseisenlem2  16074  lgseisen  16077  lgsquadlem1  16080  lgsquadlem2  16081  lgsquad2lem1  16084  lgsquad2lem2  16085  lgsquad2  16086  m1lgs  16088  2lgslem1  16094  2lgslem2  16095  2lgs  16107  2sqlem9  16127  2sqlem10  16128  ushgredgedg  16351  ushgredgedgloop  16353  uhgrspansubgrlem  16401  wlkvtxiedg  16470  wlkvtxiedgg  16471  wlk1walkdom  16484  upgr2wlkdc  16502  clwwlkccatlem  16525  umgrclwwlkge2  16527  clwwlknonmpo  16553  clwwlknonex2lem2  16563  clwwlknonex2  16564  konigsberglem1  16613  pwle2  16912  pw1nct  16917  nninfsellemdc  16928  nnnninfen  16939  nnnninfex  16940  nninfnfiinf  16941  sbthom  16946  repiecelem  16949  repiecele0  16950  trirec0  16968  apdifflemr  16971  reap0  16983  nconstwlpolem  16990