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 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  sylanblc  419  sylanblrc  420  equveli  1812  sseqtrid  3298  ssdifin0  3609  uneqdifeqim  3613  unimax  3969  opth  4379  djussxp  4927  iss  5112  relresfld  5320  eldmrexrn  5852  f1oresrab  5876  fmptco  5877  fsn  5883  fnressn  5904  foima2  5960  foeqcnvco  5999  isoini2  6028  relmptopab  6294  ofres  6321  ofco  6325  suppval1  6483  suppimacnvfn  6490  suppinisegdc  6513  tposexg  6534  tfrlemisucaccv  6601  tfrlemibex  6605  tfri1dALT  6627  tfrcl  6640  rdgivallem  6657  frecabex  6674  frectfr  6676  frecrdg  6684  pmresg  6962  mapsnd  6976  mapsn  6978  mapsncnv  6983  ixpsnf1o  7024  en1  7092  2dom  7099  mapsnend  7105  enpr2d  7117  en2  7118  mapxpen  7154  mapunen  7157  phplem4  7162  exmidpw2en  7225  fiintim  7244  sbthlem2  7282  elfir  7313  2omap  7325  infglbti  7372  caseinl  7438  caseinr  7439  difinfsnlem  7446  difinfsn  7447  nninfisollemne  7478  exmidfodomrlemim  7560  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  2omotaplemap  7630  archnqq  7791  prarloclemlt  7867  prarloclemlo  7868  prarloclemcalc  7876  recexprlemm  7998  recexprlemex  8011  caucvgprlemm  8042  caucvgprprlemmu  8069  suplocexprlem2b  8088  suplocexprlemmu  8092  suplocexprlemlub  8098  1idsr  8142  recexgt0sr  8147  archsr  8156  caucvgsrlemoffval  8170  caucvgsrlemofff  8171  caucvgsrlemoffres  8174  caucvgsr  8176  ltpsrprg  8177  suplocsrlem  8182  pitonnlem2  8221  pitonn  8222  pitoregt0  8223  pitore  8224  recnnre  8225  axrnegex  8253  nntopi  8268  msqge0  8953  mulge0  8956  recexaplem2  8989  recexap  8990  recgt0  9189  recreclt  9239  ofsubeq0  9301  nn1m1nn  9332  nn1suc  9333  nnle1eq1  9338  nn1gt1  9348  nnsub  9353  addltmul  9554  nn0le0eq0  9603  elnn0nn  9617  elnnz  9664  elznn0  9669  zlem1lt  9711  zltlem1  9712  elz2  9726  nn0n0n1ge2b  9735  nn0lt2  9737  nn0le2is012  9738  eluzaddi  9965  eluzsubi  9966  uzp1  9972  peano2uzr  10001  nn01to3  10033  qreccl  10058  irrmulap  10065  ltpnf  10199  xaddass2  10289  iccen  10426  fz01en  10476  fzpreddisj  10495  fzsuc2  10503  fseq1p1m1  10518  fseq1m1p1  10519  elfzp1b  10521  fzoss2  10598  fzval3  10639  fzosplitsnm1  10644  fzosplitprm1  10670  flhalf  10758  fldiv4lem1div2uz2  10762  modqmulnn  10800  modqmuladdnn0  10826  frec2uzrand  10863  frecuzrdg0  10871  frecuzrdg0t  10880  frecfzennn  10884  frecfzen2  10885  uzennn  10894  seqeq1  10908  seqp1g  10924  seqclg  10930  seq3m1  10931  monoord2  10944  ser3mono  10945  seqf1oglem1  10977  seqf1oglem2  10978  seqfeq4g  10989  ser0f  10992  exp3vallem  10998  expm1t  11025  expeq0  11028  expubnd  11054  binom3  11115  facndiv  11199  facavg  11206  bcn0  11215  bcnp1n  11219  bcm1k  11220  bcp1nk  11222  bcval5  11223  bcn2  11224  bcp1m1  11225  bcpasc  11226  bcn2m1  11230  hashsng  11259  hashun  11267  hashfz  11284  hashfzo  11285  hashmap  11290  hashfibclem  11304  hashf1lem1  11307  hashf1  11309  seq3coll  11316  hash2en  11317  iswrdiz  11333  snopiswrd  11336  ccat1st1st  11431  swrds1  11462  cats1un  11515  wrdind  11516  wrd2ind  11517  swrdccatin1  11519  swrdccat3blem  11533  shftfval  11608  2shfti  11618  resqrexlemf1  11796  abs00ap  11850  sqabs  11871  ltabs  11876  caubnd2  11906  max0addsup  12008  rexico  12010  mulcn2  12103  climaddc1  12120  climmulc2  12122  climsubc1  12123  climsubc2  12124  iserex  12130  climlec2  12132  iser3shft  12137  climcvg1nlem  12140  serf0  12143  sumrbdc  12171  fsumm1  12208  fsump1  12212  fsum00  12254  telfsumo  12258  fsumparts  12262  hashiun  12270  binomlem  12275  binom1dif  12279  bcxmas  12281  isumsplit  12283  isum1p  12284  arisum  12290  arisum2  12291  trireciplem  12292  explecnv  12297  geolim  12303  georeclim  12305  mertenslem2  12328  mertensabs  12329  prodf1f  12335  prodrbdclem2  12365  efcllemp  12450  ef0lem  12452  efgt0  12476  eftlub  12482  efsep  12483  effsumlt  12484  tanval3ap  12506  efi4p  12509  resin4p  12510  recos4p  12511  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  sinltxirr  12553  sin01gt0  12554  cos01gt0  12555  absefib  12563  efieq1re  12564  eirraplem  12569  dvdsdc  12590  dvdscmulr  12612  fsumdvds  12634  dvdslelemd  12635  3dvds  12656  odd2np1lem  12664  odd2np1  12665  flodddiv4  12728  bitsfzo  12747  bitsmod  12748  gcdsupex  12759  gcdsupcl  12760  gcd1  12789  nninfctlemfo  12842  nn0seqcvgd  12844  algcvg  12851  algcvgblem  12852  eucalg  12862  prmind2  12923  qden1elz  13010  dfphi2  13027  phiprm  13030  phimullem  13032  prmdiv  13042  prmdiveq  13043  prm23lt5  13071  pcpre1  13100  pczpre  13105  pcdiv  13110  pc1  13113  pcqdiv  13115  pcexp  13117  pcxnn0cl  13118  pcxcl  13119  pcdvdstr  13135  pc2dvds  13138  sumhashdc  13155  fldivp1  13156  pcfaclem  13157  qexpz  13160  expnprm  13161  prmpwdvds  13163  pockthlem  13164  4sqlem5  13190  4sqlem6  13191  4sqlem11  13209  4sqlem13m  13211  4sqlem19  13217  prmlem1a  13250  ballotfilemofi  13277  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilemscl  13305  ballotfilemsle  13306  oddennn  13341  xpct  13345  ennnfonelemj0  13350  ennnfonelemen  13370  ctinfomlemom  13376  omctfn  13392  restid  13663  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfnlemg  13694  xpscf  13727  gzsumvalx  13768  gzsumsplit1r  13774  gzsumcl  13863  mulgnngzsum  13989  mulgnndir  14013  mulgneg2  14018  cntrnsg  14176  gsumvalfi  14242  gsum2dfilem2  14272  prdsex  14279  prdsval  14280  prdsbaslemss  14281  prdsbas  14283  prdsgrpd  14304  prdsinvgd  14305  dvdsrmuld  14512  zsssubrg  15031  znval  15080  znle  15081  znbaslemnn  15083  znf1o  15095  znleval  15097  psrval  15161  psrlidmfi  15219  psrridmfi  15220  mplsubgfileminv  15247  mplsubrglemcl  15249  restuni2  15436  cnrest2r  15496  lmfss  15503  lmres  15507  lmtopcnp  15509  ispsmet  15582  isxmet2d  15607  ismet2  15613  blfvalps  15644  blex  15646  xblss2  15664  reopnap  15805  divcnap  15824  climcncf  15843  cncfmpt2fcntop  15858  hovera  15906  limcdifap  15921  cnplimcim  15926  cnlimcim  15930  cnlimc  15931  cnlimci  15932  dvbss  15944  dvcnp2cntop  15958  dvcn  15959  dvaddxxbr  15960  dvmulxxbr  15961  dvexp  15970  dveflem  15985  plyval  15991  elply2  15994  plyf  15996  plyss  15997  plyssc  15998  elplyr  15999  plyaddlem1  16006  plymullem1  16007  plyaddlem  16008  plymullem  16009  plyco  16018  plycj  16020  dvply1  16024  reeff1olem  16030  sinperlem  16068  sin2kpi  16071  cos2kpi  16072  sin2pim  16073  cos2pim  16074  cosq14gt0  16092  coseq0q4123  16094  tangtx  16098  abssinper  16106  sinkpi  16107  coskpi  16108  cosq34lt1  16111  logrpap0b  16139  logdivlti  16144  rpcxpsqrtth  16198  rpabscxpbnd  16208  binom4  16252  birthdaylem2  16259  birthdaylem3  16260  wilthlem1  16265  0sgm  16287  ppiprm  16292  ppinprm  16293  chtprm  16294  chtnprm  16295  chtdif  16297  ppiqp1le  16300  ppidif  16302  ppiqeq0  16313  ppiqltx  16314  prmorcht  16315  1sgmprm  16321  1sgm2ppw  16322  ppiublem2  16325  ppiqub  16326  chtublem  16328  chtqub  16329  mersenne  16330  perfect1  16331  perfectlem1  16332  perfectlem2  16333  perfect  16334  bcp1ctr  16339  bclbnd  16340  bposlem1  16344  bposlem2  16345  bposlem3  16346  bposlem4  16347  bposlem5  16348  bposlem6  16349  bposlem9  16352  bpos  16353  lgslem1  16357  lgsval  16361  lgsfvalg  16362  lgsfcl2  16363  lgsfcl  16365  lgsval2lem  16367  lgsvalmod  16376  lgsneg  16381  lgsdilem  16384  lgsdir2lem3  16387  lgsdir  16392  lgsdilem2  16393  lgsdi  16394  lgsne0  16395  lgsabs1  16396  lgsprme0  16399  lgsdirnn0  16404  lgsdinn0  16405  gausslemma2dlem0d  16409  gausslemma2dlem1a  16415  gausslemma2dlem1f1o  16417  gausslemma2dlem3  16420  gausslemma2dlem4  16421  gausslemma2dlem5a  16422  gausslemma2dlem5  16423  gausslemma2dlem6  16424  lgseisenlem2  16428  lgseisen  16431  lgsquadlem1  16434  lgsquadlem2  16435  lgsquad2lem1  16438  lgsquad2lem2  16439  lgsquad2  16440  m1lgs  16442  2lgslem1  16448  2lgslem2  16449  2lgs  16461  2sqlem9  16481  2sqlem10  16482  ushgredgedg  16705  ushgredgedgloop  16707  uhgrspansubgrlem  16755  wlkvtxiedg  16824  wlkvtxiedgg  16825  wlk1walkdom  16838  upgr2wlkdc  16856  clwwlkccatlem  16879  umgrclwwlkge2  16881  clwwlknonmpo  16907  clwwlknonex2lem2  16917  clwwlknonex2  16918  konigsberglem1  16967  pwle2  17266  pw1nct  17271  nninfsellemdc  17292  nnnninfen  17303  nnnninfex  17304  nninfnfiinf  17305  sbthom  17310  repiecelem  17313  repiecele0  17314  trirec0  17333  apdifflemr  17336  reap0  17348  nconstwlpolem  17355