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  8907  mulge0  8910  recexaplem2  8943  recexap  8944  recgt0  9141  recreclt  9191  nn1m1nn  9272  nn1suc  9273  nnle1eq1  9278  nn1gt1  9288  nnsub  9293  addltmul  9492  nn0le0eq0  9541  elnn0nn  9555  elnnz  9604  elznn0  9609  zlem1lt  9651  zltlem1  9652  elz2  9666  nn0n0n1ge2b  9675  nn0lt2  9677  nn0le2is012  9678  eluzaddi  9899  eluzsubi  9900  uzp1  9906  peano2uzr  9935  nn01to3  9967  qreccl  9992  irrmulap  9998  ltpnf  10132  xaddass2  10222  iccen  10359  fz01en  10408  fzpreddisj  10427  fzsuc2  10435  fseq1p1m1  10450  fseq1m1p1  10451  elfzp1b  10453  fzoss2  10530  fzval3  10571  fzosplitsnm1  10576  fzosplitprm1  10602  flhalf  10686  fldiv4lem1div2uz2  10690  modqmulnn  10728  modqmuladdnn0  10754  frec2uzrand  10791  frecuzrdg0  10799  frecuzrdg0t  10808  frecfzennn  10812  frecfzen2  10813  uzennn  10822  seqeq1  10836  seqp1g  10852  seqclg  10858  seq3m1  10859  monoord2  10872  ser3mono  10873  seqf1oglem1  10905  seqf1oglem2  10906  seqfeq4g  10917  ser0f  10920  exp3vallem  10926  expm1t  10953  expeq0  10956  expubnd  10982  binom3  11043  facndiv  11126  facavg  11133  bcn0  11142  bcnp1n  11146  bcm1k  11147  bcp1nk  11149  bcval5  11150  bcn2  11151  bcp1m1  11152  bcpasc  11153  bcn2m1  11157  hashsng  11186  hashun  11194  hashfz  11211  hashfzo  11212  hashmap  11217  hashfibclem  11231  seq3coll  11239  hash2en  11240  iswrdiz  11256  snopiswrd  11259  ccat1st1st  11354  swrds1  11385  cats1un  11438  wrdind  11439  wrd2ind  11440  swrdccatin1  11442  swrdccat3blem  11456  shftfval  11531  2shfti  11541  resqrexlemf1  11718  abs00ap  11772  sqabs  11792  ltabs  11797  caubnd2  11827  max0addsup  11929  rexico  11931  mulcn2  12022  climaddc1  12039  climmulc2  12041  climsubc1  12042  climsubc2  12043  iserex  12049  climlec2  12051  iser3shft  12056  climcvg1nlem  12059  serf0  12062  sumrbdc  12090  fsumm1  12127  fsump1  12131  fsum00  12173  telfsumo  12177  fsumparts  12181  hashiun  12189  binomlem  12194  binom1dif  12198  bcxmas  12200  isumsplit  12202  isum1p  12203  arisum  12209  arisum2  12210  trireciplem  12211  explecnv  12216  geolim  12222  georeclim  12224  mertenslem2  12247  mertensabs  12248  prodf1f  12254  prodrbdclem2  12284  efcllemp  12369  ef0lem  12371  efgt0  12395  eftlub  12401  efsep  12402  effsumlt  12403  tanval3ap  12425  efi4p  12428  resin4p  12429  recos4p  12430  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sinltxirr  12472  sin01gt0  12473  cos01gt0  12474  absefib  12482  efieq1re  12483  eirraplem  12488  dvdsdc  12509  dvdscmulr  12531  fsumdvds  12553  dvdslelemd  12554  3dvds  12575  odd2np1lem  12583  odd2np1  12584  flodddiv4  12647  bitsfzo  12666  bitsmod  12667  gcdsupex  12678  gcdsupcl  12679  gcd1  12708  nninfctlemfo  12761  nn0seqcvgd  12763  algcvg  12770  algcvgblem  12771  eucalg  12781  prmind2  12842  qden1elz  12927  dfphi2  12942  phiprm  12945  phimullem  12947  prmdiv  12957  prmdiveq  12958  prm23lt5  12986  pcpre1  13015  pczpre  13020  pcdiv  13025  pc1  13028  pcqdiv  13030  pcexp  13032  pcxnn0cl  13033  pcxcl  13034  pcdvdstr  13050  pc2dvds  13053  sumhashdc  13070  fldivp1  13071  pcfaclem  13072  qexpz  13075  expnprm  13076  prmpwdvds  13078  pockthlem  13079  4sqlem5  13105  4sqlem6  13106  4sqlem11  13124  4sqlem13m  13126  4sqlem19  13132  ballotfilemofi  13163  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  ballotfilemscl  13191  ballotfilemsle  13192  oddennn  13227  xpct  13231  ennnfonelemj0  13236  ennnfonelemen  13256  ctinfomlemom  13262  omctfn  13278  restid  13547  prdsex  13566  prdsval  13570  prdsbaslemss  13571  prdsbas  13573  imasbas  13604  imasplusg  13605  imasmulr  13606  imasaddfnlemg  13611  xpscf  13644  igsumvalx  13686  gsumsplit1r  13695  gsumprval  13696  gsumfzz  13792  gsumfzcl  13796  prdsgrpd  13906  prdsinvgd  13907  mulgnngsum  13928  mulgnndir  13952  mulgneg2  13957  dvdsrmuld  14326  zsssubrg  14845  znval  14896  znle  14897  znbaslemnn  14899  znf1o  14911  znleval  14913  psrval  14926  restuni2  15154  cnrest2r  15214  lmfss  15221  lmres  15225  lmtopcnp  15227  ispsmet  15300  isxmet2d  15325  ismet2  15331  blfvalps  15362  blex  15364  xblss2  15382  reopnap  15523  divcnap  15542  climcncf  15561  cncfmpt2fcntop  15576  hovera  15624  limcdifap  15639  cnplimcim  15644  cnlimcim  15648  cnlimc  15649  cnlimci  15650  dvbss  15662  dvcnp2cntop  15676  dvcn  15677  dvaddxxbr  15678  dvmulxxbr  15679  dvexp  15688  dveflem  15703  plyval  15709  elply2  15712  plyf  15714  plyss  15715  plyssc  15716  elplyr  15717  plyaddlem1  15724  plymullem1  15725  plyaddlem  15726  plymullem  15727  plyco  15736  plycj  15738  dvply1  15742  reeff1olem  15748  sinperlem  15785  sin2kpi  15788  cos2kpi  15789  sin2pim  15790  cos2pim  15791  cosq14gt0  15809  coseq0q4123  15811  tangtx  15815  abssinper  15823  sinkpi  15824  coskpi  15825  cosq34lt1  15827  logrpap0b  15853  logdivlti  15858  rpcxpsqrtth  15907  rpabscxpbnd  15917  binom4  15956  wilthlem1  15960  0sgm  15965  1sgmprm  15974  1sgm2ppw  15975  mersenne  15977  perfect1  15978  perfectlem1  15979  perfectlem2  15980  perfect  15981  lgslem1  15985  lgsval  15989  lgsfvalg  15990  lgsfcl2  15991  lgsfcl  15993  lgsval2lem  15995  lgsvalmod  16004  lgsneg  16009  lgsdilem  16012  lgsdir2lem3  16015  lgsdir  16020  lgsdilem2  16021  lgsdi  16022  lgsne0  16023  lgsabs1  16024  lgsprme0  16027  lgsdirnn0  16032  lgsdinn0  16033  gausslemma2dlem0d  16037  gausslemma2dlem1a  16043  gausslemma2dlem1f1o  16045  gausslemma2dlem3  16048  gausslemma2dlem4  16049  gausslemma2dlem5a  16050  gausslemma2dlem5  16051  gausslemma2dlem6  16052  lgseisenlem2  16056  lgseisen  16059  lgsquadlem1  16062  lgsquadlem2  16063  lgsquad2lem1  16066  lgsquad2lem2  16067  lgsquad2  16068  m1lgs  16070  2lgslem1  16076  2lgslem2  16077  2lgs  16089  2sqlem9  16109  2sqlem10  16110  ushgredgedg  16333  ushgredgedgloop  16335  uhgrspansubgrlem  16383  wlkvtxiedg  16452  wlkvtxiedgg  16453  wlk1walkdom  16466  upgr2wlkdc  16484  clwwlkccatlem  16507  umgrclwwlkge2  16509  clwwlknonmpo  16535  clwwlknonex2lem2  16545  clwwlknonex2  16546  konigsberglem1  16595  pwle2  16884  pw1nct  16889  nninfsellemdc  16900  nnnninfen  16911  nnnninfex  16912  nninfnfiinf  16913  sbthom  16918  repiecelem  16921  repiecele0  16922  trirec0  16940  apdifflemr  16943  reap0  16955  trimul0or  16957  nconstwlpolem  16963  gfsumval  16974