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  tposexg  6533  tfrlemisucaccv  6600  tfrlemibex  6604  tfri1dALT  6626  tfrcl  6639  rdgivallem  6656  frecabex  6673  frectfr  6675  frecrdg  6683  pmresg  6961  mapsnd  6975  mapsn  6977  mapsncnv  6982  ixpsnf1o  7023  en1  7091  2dom  7098  mapsnend  7104  enpr2d  7116  en2  7117  mapxpen  7153  mapunen  7156  phplem4  7161  exmidpw2en  7224  fiintim  7243  sbthlem2  7281  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  9666  elznn0  9671  zlem1lt  9713  zltlem1  9714  elz2  9728  nn0n0n1ge2b  9737  nn0lt2  9739  nn0le2is012  9740  eluzaddi  9966  eluzsubi  9967  uzp1  9973  peano2uzr  10002  nn01to3  10034  qreccl  10059  irrmulap  10066  ltpnf  10200  xaddass2  10290  iccen  10427  fz01en  10477  fzpreddisj  10496  fzsuc2  10504  fseq1p1m1  10519  fseq1m1p1  10520  elfzp1b  10522  fzoss2  10599  fzval3  10640  fzosplitsnm1  10645  fzosplitprm1  10671  flhalf  10759  fldiv4lem1div2uz2  10763  modqmulnn  10801  modqmuladdnn0  10827  frec2uzrand  10864  frecuzrdg0  10872  frecuzrdg0t  10881  frecfzennn  10885  frecfzen2  10886  uzennn  10895  seqeq1  10909  seqp1g  10925  seqclg  10931  seq3m1  10932  monoord2  10945  ser3mono  10946  seqf1oglem1  10978  seqf1oglem2  10979  seqfeq4g  10990  ser0f  10993  exp3vallem  10999  expm1t  11026  expeq0  11029  expubnd  11055  binom3  11116  facndiv  11200  facavg  11207  bcn0  11216  bcnp1n  11220  bcm1k  11221  bcp1nk  11223  bcval5  11224  bcn2  11225  bcp1m1  11226  bcpasc  11227  bcn2m1  11231  hashsng  11260  hashun  11268  hashfz  11285  hashfzo  11286  hashmap  11291  hashfibclem  11305  hashf1lem1  11308  hashf1  11310  seq3coll  11317  hash2en  11318  iswrdiz  11334  snopiswrd  11337  ccat1st1st  11432  swrds1  11463  cats1un  11516  wrdind  11517  wrd2ind  11518  swrdccatin1  11520  swrdccat3blem  11534  shftfval  11609  2shfti  11619  resqrexlemf1  11797  abs00ap  11851  sqabs  11872  ltabs  11877  caubnd2  11907  max0addsup  12009  rexico  12011  mulcn2  12104  climaddc1  12121  climmulc2  12123  climsubc1  12124  climsubc2  12125  iserex  12131  climlec2  12133  iser3shft  12138  climcvg1nlem  12141  serf0  12144  sumrbdc  12172  fsumm1  12209  fsump1  12213  fsum00  12255  telfsumo  12259  fsumparts  12263  hashiun  12271  binomlem  12276  binom1dif  12280  bcxmas  12282  isumsplit  12284  isum1p  12285  arisum  12291  arisum2  12292  trireciplem  12293  explecnv  12298  geolim  12304  georeclim  12306  mertenslem2  12329  mertensabs  12330  prodf1f  12336  prodrbdclem2  12366  efcllemp  12451  ef0lem  12453  efgt0  12477  eftlub  12483  efsep  12484  effsumlt  12485  tanval3ap  12507  efi4p  12510  resin4p  12511  recos4p  12512  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  sinltxirr  12554  sin01gt0  12555  cos01gt0  12556  absefib  12564  efieq1re  12565  eirraplem  12570  dvdsdc  12591  dvdscmulr  12613  fsumdvds  12635  dvdslelemd  12636  3dvds  12657  odd2np1lem  12665  odd2np1  12666  flodddiv4  12729  bitsfzo  12748  bitsmod  12749  gcdsupex  12760  gcdsupcl  12761  gcd1  12790  nninfctlemfo  12843  nn0seqcvgd  12845  algcvg  12852  algcvgblem  12853  eucalg  12863  prmind2  12924  qden1elz  13011  dfphi2  13028  phiprm  13031  phimullem  13033  prmdiv  13043  prmdiveq  13044  prm23lt5  13072  pcpre1  13101  pczpre  13106  pcdiv  13111  pc1  13114  pcqdiv  13116  pcexp  13118  pcxnn0cl  13119  pcxcl  13120  pcdvdstr  13136  pc2dvds  13139  sumhashdc  13156  fldivp1  13157  pcfaclem  13158  qexpz  13161  expnprm  13162  prmpwdvds  13164  pockthlem  13165  4sqlem5  13191  4sqlem6  13192  4sqlem11  13210  4sqlem13m  13212  4sqlem19  13218  prmlem1a  13251  ballotfilemofi  13278  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemodife  13299  ballotfilemscl  13306  ballotfilemsle  13307  oddennn  13342  xpct  13346  ennnfonelemj0  13351  ennnfonelemen  13371  ctinfomlemom  13377  omctfn  13393  restid  13664  imasbas  13688  imasplusg  13689  imasmulr  13690  imasaddfnlemg  13695  xpscf  13728  gzsumvalx  13769  gzsumsplit1r  13775  gzsumcl  13864  mulgnngzsum  13990  mulgnndir  14014  mulgneg2  14019  cntrnsg  14177  gsumvalfi  14243  gsum2dfilem2  14273  prdsex  14280  prdsval  14281  prdsbaslemss  14282  prdsbas  14284  prdsgrpd  14305  prdsinvgd  14306  dvdsrmuld  14513  zsssubrg  15032  znval  15081  znle  15082  znbaslemnn  15084  znf1o  15096  znleval  15098  psrval  15162  psrlidmfi  15204  psrridmfi  15205  restuni2  15415  cnrest2r  15475  lmfss  15482  lmres  15486  lmtopcnp  15488  ispsmet  15561  isxmet2d  15586  ismet2  15592  blfvalps  15623  blex  15625  xblss2  15643  reopnap  15784  divcnap  15803  climcncf  15822  cncfmpt2fcntop  15837  hovera  15885  limcdifap  15900  cnplimcim  15905  cnlimcim  15909  cnlimc  15910  cnlimci  15911  dvbss  15923  dvcnp2cntop  15937  dvcn  15938  dvaddxxbr  15939  dvmulxxbr  15940  dvexp  15949  dveflem  15964  plyval  15970  elply2  15973  plyf  15975  plyss  15976  plyssc  15977  elplyr  15978  plyaddlem1  15985  plymullem1  15986  plyaddlem  15987  plymullem  15988  plyco  15997  plycj  15999  dvply1  16003  reeff1olem  16009  sinperlem  16047  sin2kpi  16050  cos2kpi  16051  sin2pim  16052  cos2pim  16053  cosq14gt0  16071  coseq0q4123  16073  tangtx  16077  abssinper  16085  sinkpi  16086  coskpi  16087  cosq34lt1  16090  logrpap0b  16118  logdivlti  16123  rpcxpsqrtth  16177  rpabscxpbnd  16187  binom4  16231  birthdaylem2  16238  birthdaylem3  16239  wilthlem1  16244  0sgm  16266  ppiprm  16271  ppinprm  16272  chtprm  16273  chtnprm  16274  chtdif  16276  ppiqp1le  16279  ppidif  16281  ppiqeq0  16292  ppiqltx  16293  prmorcht  16294  1sgmprm  16300  1sgm2ppw  16301  ppiublem2  16304  ppiqub  16305  chtublem  16307  chtqub  16308  mersenne  16309  perfect1  16310  perfectlem1  16311  perfectlem2  16312  perfect  16313  bcp1ctr  16318  bclbnd  16319  bposlem1  16323  bposlem2  16324  bposlem3  16325  bposlem4  16326  bposlem5  16327  bposlem6  16328  bposlem9  16331  bpos  16332  lgslem1  16336  lgsval  16340  lgsfvalg  16341  lgsfcl2  16342  lgsfcl  16344  lgsval2lem  16346  lgsvalmod  16355  lgsneg  16360  lgsdilem  16363  lgsdir2lem3  16366  lgsdir  16371  lgsdilem2  16372  lgsdi  16373  lgsne0  16374  lgsabs1  16375  lgsprme0  16378  lgsdirnn0  16383  lgsdinn0  16384  gausslemma2dlem0d  16388  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  gausslemma2dlem3  16399  gausslemma2dlem4  16400  gausslemma2dlem5a  16401  gausslemma2dlem5  16402  gausslemma2dlem6  16403  lgseisenlem2  16407  lgseisen  16410  lgsquadlem1  16413  lgsquadlem2  16414  lgsquad2lem1  16417  lgsquad2lem2  16418  lgsquad2  16419  m1lgs  16421  2lgslem1  16427  2lgslem2  16428  2lgs  16440  2sqlem9  16460  2sqlem10  16461  ushgredgedg  16684  ushgredgedgloop  16686  uhgrspansubgrlem  16734  wlkvtxiedg  16803  wlkvtxiedgg  16804  wlk1walkdom  16817  upgr2wlkdc  16835  clwwlkccatlem  16858  umgrclwwlkge2  16860  clwwlknonmpo  16886  clwwlknonex2lem2  16896  clwwlknonex2  16897  konigsberglem1  16946  pwle2  17245  pw1nct  17250  nninfsellemdc  17271  nnnninfen  17282  nnnninfex  17283  nninfnfiinf  17284  sbthom  17289  repiecelem  17292  repiecele0  17293  trirec0  17312  apdifflemr  17315  reap0  17327  nconstwlpolem  17334