Theorem sylancl 417

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 415	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  419  sylanblrc  420  equveli  1812  sseqtrid  3298  ssdifin0  3609  uneqdifeqim  3613  unimax  3967  opth  4375  djussxp  4923  iss  5107  relresfld  5315  eldmrexrn  5843  f1oresrab  5867  fmptco  5868  fsn  5874  fnressn  5895  foima2  5951  foeqcnvco  5990  isoini2  6019  relmptopab  6285  ofres  6311  ofco  6315  suppval1  6473  suppimacnvfn  6480  tposexg  6523  tfrlemisucaccv  6590  tfrlemibex  6594  tfri1dALT  6616  tfrcl  6629  rdgivallem  6646  frecabex  6663  frectfr  6665  frecrdg  6673  pmresg  6951  mapsnd  6964  mapsn  6966  mapsncnv  6971  ixpsnf1o  7012  en1  7080  2dom  7087  mapsnend  7093  enpr2d  7105  en2  7106  mapxpen  7142  mapunen  7145  phplem4  7150  exmidpw2en  7213  fiintim  7232  sbthlem2  7269  elfir  7301  2omap  7312  infglbti  7359  caseinl  7425  caseinr  7426  difinfsnlem  7433  difinfsn  7434  nninfisollemne  7465  exmidfodomrlemim  7547  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  2omotaplemap  7617  archnqq  7778  prarloclemlt  7854  prarloclemlo  7855  prarloclemcalc  7863  recexprlemm  7985  recexprlemex  7998  caucvgprlemm  8029  caucvgprprlemmu  8056  suplocexprlem2b  8075  suplocexprlemmu  8079  suplocexprlemlub  8085  1idsr  8129  recexgt0sr  8134  archsr  8143  caucvgsrlemoffval  8157  caucvgsrlemofff  8158  caucvgsrlemoffres  8161  caucvgsr  8163  ltpsrprg  8164  suplocsrlem  8169  pitonnlem2  8208  pitonn  8209  pitoregt0  8210  pitore  8211  recnnre  8212  axrnegex  8240  nntopi  8255  msqge0  8938  mulge0  8941  recexaplem2  8974  recexap  8975  recgt0  9174  recreclt  9224  nn1m1nn  9305  nn1suc  9306  nnle1eq1  9311  nn1gt1  9321  nnsub  9326  addltmul  9525  nn0le0eq0  9574  elnn0nn  9588  elnnz  9637  elznn0  9642  zlem1lt  9684  zltlem1  9685  elz2  9699  nn0n0n1ge2b  9708  nn0lt2  9710  nn0le2is012  9711  eluzaddi  9932  eluzsubi  9933  uzp1  9939  peano2uzr  9968  nn01to3  10000  qreccl  10025  irrmulap  10031  ltpnf  10165  xaddass2  10255  iccen  10392  fz01en  10442  fzpreddisj  10461  fzsuc2  10469  fseq1p1m1  10484  fseq1m1p1  10485  elfzp1b  10487  fzoss2  10564  fzval3  10605  fzosplitsnm1  10610  fzosplitprm1  10636  flhalf  10720  fldiv4lem1div2uz2  10724  modqmulnn  10762  modqmuladdnn0  10788  frec2uzrand  10825  frecuzrdg0  10833  frecuzrdg0t  10842  frecfzennn  10846  frecfzen2  10847  uzennn  10856  seqeq1  10870  seqp1g  10886  seqclg  10892  seq3m1  10893  monoord2  10906  ser3mono  10907  seqf1oglem1  10939  seqf1oglem2  10940  seqfeq4g  10951  ser0f  10954  exp3vallem  10960  expm1t  10987  expeq0  10990  expubnd  11016  binom3  11077  facndiv  11160  facavg  11167  bcn0  11176  bcnp1n  11180  bcm1k  11181  bcp1nk  11183  bcval5  11184  bcn2  11185  bcp1m1  11186  bcpasc  11187  bcn2m1  11191  hashsng  11220  hashun  11228  hashfz  11245  hashfzo  11246  hashmap  11251  hashfibclem  11265  hashf1lem1  11268  hashf1  11270  seq3coll  11277  hash2en  11278  iswrdiz  11294  snopiswrd  11297  ccat1st1st  11392  swrds1  11423  cats1un  11476  wrdind  11477  wrd2ind  11478  swrdccatin1  11480  swrdccat3blem  11494  shftfval  11569  2shfti  11579  resqrexlemf1  11757  abs00ap  11811  sqabs  11831  ltabs  11836  caubnd2  11866  max0addsup  11968  rexico  11970  mulcn2  12061  climaddc1  12078  climmulc2  12080  climsubc1  12081  climsubc2  12082  iserex  12088  climlec2  12090  iser3shft  12095  climcvg1nlem  12098  serf0  12101  sumrbdc  12129  fsumm1  12166  fsump1  12170  fsum00  12212  telfsumo  12216  fsumparts  12220  hashiun  12228  binomlem  12233  binom1dif  12237  bcxmas  12239  isumsplit  12241  isum1p  12242  arisum  12248  arisum2  12249  trireciplem  12250  explecnv  12255  geolim  12261  georeclim  12263  mertenslem2  12286  mertensabs  12287  prodf1f  12293  prodrbdclem2  12323  efcllemp  12408  ef0lem  12410  efgt0  12434  eftlub  12440  efsep  12441  effsumlt  12442  tanval3ap  12464  efi4p  12467  resin4p  12468  recos4p  12469  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  sinltxirr  12511  sin01gt0  12512  cos01gt0  12513  absefib  12521  efieq1re  12522  eirraplem  12527  dvdsdc  12548  dvdscmulr  12570  fsumdvds  12592  dvdslelemd  12593  3dvds  12614  odd2np1lem  12622  odd2np1  12623  flodddiv4  12686  bitsfzo  12705  bitsmod  12706  gcdsupex  12717  gcdsupcl  12718  gcd1  12747  nninfctlemfo  12800  nn0seqcvgd  12802  algcvg  12809  algcvgblem  12810  eucalg  12820  prmind2  12881  qden1elz  12966  dfphi2  12981  phiprm  12984  phimullem  12986  prmdiv  12996  prmdiveq  12997  prm23lt5  13025  pcpre1  13054  pczpre  13059  pcdiv  13064  pc1  13067  pcqdiv  13069  pcexp  13071  pcxnn0cl  13072  pcxcl  13073  pcdvdstr  13089  pc2dvds  13092  sumhashdc  13109  fldivp1  13110  pcfaclem  13111  qexpz  13114  expnprm  13115  prmpwdvds  13117  pockthlem  13118  4sqlem5  13144  4sqlem6  13145  4sqlem11  13163  4sqlem13m  13165  4sqlem19  13171  ballotfilemofi  13202  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemodife  13223  ballotfilemscl  13230  ballotfilemsle  13231  oddennn  13266  xpct  13270  ennnfonelemj0  13275  ennnfonelemen  13295  ctinfomlemom  13301  omctfn  13317  restid  13587  imasbas  13611  imasplusg  13612  imasmulr  13613  imasaddfnlemg  13618  xpscf  13651  gzsumvalx  13692  gzsumsplit1r  13698  gzsumcl  13787  mulgnngzsum  13913  mulgnndir  13937  mulgneg2  13942  gsumvalfi  14135  prdsex  14155  prdsval  14156  prdsbaslemss  14157  prdsbas  14159  prdsgrpd  14180  prdsinvgd  14181  dvdsrmuld  14386  zsssubrg  14905  znval  14954  znle  14955  znbaslemnn  14957  znf1o  14969  znleval  14971  psrval  15033  restuni2  15261  cnrest2r  15321  lmfss  15328  lmres  15332  lmtopcnp  15334  ispsmet  15407  isxmet2d  15432  ismet2  15438  blfvalps  15469  blex  15471  xblss2  15489  reopnap  15630  divcnap  15649  climcncf  15668  cncfmpt2fcntop  15683  hovera  15731  limcdifap  15746  cnplimcim  15751  cnlimcim  15755  cnlimc  15756  cnlimci  15757  dvbss  15769  dvcnp2cntop  15783  dvcn  15784  dvaddxxbr  15785  dvmulxxbr  15786  dvexp  15795  dveflem  15810  plyval  15816  elply2  15819  plyf  15821  plyss  15822  plyssc  15823  elplyr  15824  plyaddlem1  15831  plymullem1  15832  plyaddlem  15833  plymullem  15834  plyco  15843  plycj  15845  dvply1  15849  reeff1olem  15855  sinperlem  15892  sin2kpi  15895  cos2kpi  15896  sin2pim  15897  cos2pim  15898  cosq14gt0  15916  coseq0q4123  15918  tangtx  15922  abssinper  15930  sinkpi  15931  coskpi  15932  cosq34lt1  15934  logrpap0b  15960  logdivlti  15965  rpcxpsqrtth  16015  rpabscxpbnd  16025  binom4  16064  birthdaylem2  16071  birthdaylem3  16072  wilthlem1  16077  0sgm  16082  1sgmprm  16091  1sgm2ppw  16092  mersenne  16094  perfect1  16095  perfectlem1  16096  perfectlem2  16097  perfect  16098  lgslem1  16102  lgsval  16106  lgsfvalg  16107  lgsfcl2  16108  lgsfcl  16110  lgsval2lem  16112  lgsvalmod  16121  lgsneg  16126  lgsdilem  16129  lgsdir2lem3  16132  lgsdir  16137  lgsdilem2  16138  lgsdi  16139  lgsne0  16140  lgsabs1  16141  lgsprme0  16144  lgsdirnn0  16149  lgsdinn0  16150  gausslemma2dlem0d  16154  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  gausslemma2dlem3  16165  gausslemma2dlem4  16166  gausslemma2dlem5a  16167  gausslemma2dlem5  16168  gausslemma2dlem6  16169  lgseisenlem2  16173  lgseisen  16176  lgsquadlem1  16179  lgsquadlem2  16180  lgsquad2lem1  16183  lgsquad2lem2  16184  lgsquad2  16185  m1lgs  16187  2lgslem1  16193  2lgslem2  16194  2lgs  16206  2sqlem9  16226  2sqlem10  16227  ushgredgedg  16450  ushgredgedgloop  16452  uhgrspansubgrlem  16500  wlkvtxiedg  16569  wlkvtxiedgg  16570  wlk1walkdom  16583  upgr2wlkdc  16601  clwwlkccatlem  16624  umgrclwwlkge2  16626  clwwlknonmpo  16652  clwwlknonex2lem2  16662  clwwlknonex2  16663  konigsberglem1  16712  pwle2  17011  pw1nct  17016  nninfsellemdc  17027  nnnninfen  17038  nnnninfex  17039  nninfnfiinf  17040  sbthom  17045  repiecelem  17048  repiecele0  17049  trirec0  17067  apdifflemr  17070  reap0  17082  nconstwlpolem  17089