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  4377  djussxp  4925  iss  5109  relresfld  5317  eldmrexrn  5849  f1oresrab  5873  fmptco  5874  fsn  5880  fnressn  5901  foima2  5957  foeqcnvco  5996  isoini2  6025  relmptopab  6291  ofres  6317  ofco  6321  suppval1  6479  suppimacnvfn  6486  tposexg  6529  tfrlemisucaccv  6596  tfrlemibex  6600  tfri1dALT  6622  tfrcl  6635  rdgivallem  6652  frecabex  6669  frectfr  6671  frecrdg  6679  pmresg  6957  mapsnd  6970  mapsn  6972  mapsncnv  6977  ixpsnf1o  7018  en1  7086  2dom  7093  mapsnend  7099  enpr2d  7111  en2  7112  mapxpen  7148  mapunen  7151  phplem4  7156  exmidpw2en  7219  fiintim  7238  sbthlem2  7275  elfir  7307  2omap  7319  infglbti  7366  caseinl  7432  caseinr  7433  difinfsnlem  7440  difinfsn  7441  nninfisollemne  7472  exmidfodomrlemim  7554  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  2omotaplemap  7624  archnqq  7785  prarloclemlt  7861  prarloclemlo  7862  prarloclemcalc  7870  recexprlemm  7992  recexprlemex  8005  caucvgprlemm  8036  caucvgprprlemmu  8063  suplocexprlem2b  8082  suplocexprlemmu  8086  suplocexprlemlub  8092  1idsr  8136  recexgt0sr  8141  archsr  8150  caucvgsrlemoffval  8164  caucvgsrlemofff  8165  caucvgsrlemoffres  8168  caucvgsr  8170  ltpsrprg  8171  suplocsrlem  8176  pitonnlem2  8215  pitonn  8216  pitoregt0  8217  pitore  8218  recnnre  8219  axrnegex  8247  nntopi  8262  msqge0  8947  mulge0  8950  recexaplem2  8983  recexap  8984  recgt0  9183  recreclt  9233  nn1m1nn  9325  nn1suc  9326  nnle1eq1  9331  nn1gt1  9341  nnsub  9346  addltmul  9547  nn0le0eq0  9596  elnn0nn  9610  elnnz  9659  elznn0  9664  zlem1lt  9706  zltlem1  9707  elz2  9721  nn0n0n1ge2b  9730  nn0lt2  9732  nn0le2is012  9733  eluzaddi  9959  eluzsubi  9960  uzp1  9966  peano2uzr  9995  nn01to3  10027  qreccl  10052  irrmulap  10059  ltpnf  10193  xaddass2  10283  iccen  10420  fz01en  10470  fzpreddisj  10489  fzsuc2  10497  fseq1p1m1  10512  fseq1m1p1  10513  elfzp1b  10515  fzoss2  10592  fzval3  10633  fzosplitsnm1  10638  fzosplitprm1  10664  flhalf  10751  fldiv4lem1div2uz2  10755  modqmulnn  10793  modqmuladdnn0  10819  frec2uzrand  10856  frecuzrdg0  10864  frecuzrdg0t  10873  frecfzennn  10877  frecfzen2  10878  uzennn  10887  seqeq1  10901  seqp1g  10917  seqclg  10923  seq3m1  10924  monoord2  10937  ser3mono  10938  seqf1oglem1  10970  seqf1oglem2  10971  seqfeq4g  10982  ser0f  10985  exp3vallem  10991  expm1t  11018  expeq0  11021  expubnd  11047  binom3  11108  facndiv  11192  facavg  11199  bcn0  11208  bcnp1n  11212  bcm1k  11213  bcp1nk  11215  bcval5  11216  bcn2  11217  bcp1m1  11218  bcpasc  11219  bcn2m1  11223  hashsng  11252  hashun  11260  hashfz  11277  hashfzo  11278  hashmap  11283  hashfibclem  11297  hashf1lem1  11300  hashf1  11302  seq3coll  11309  hash2en  11310  iswrdiz  11326  snopiswrd  11329  ccat1st1st  11424  swrds1  11455  cats1un  11508  wrdind  11509  wrd2ind  11510  swrdccatin1  11512  swrdccat3blem  11526  shftfval  11601  2shfti  11611  resqrexlemf1  11789  abs00ap  11843  sqabs  11864  ltabs  11869  caubnd2  11899  max0addsup  12001  rexico  12003  mulcn2  12096  climaddc1  12113  climmulc2  12115  climsubc1  12116  climsubc2  12117  iserex  12123  climlec2  12125  iser3shft  12130  climcvg1nlem  12133  serf0  12136  sumrbdc  12164  fsumm1  12201  fsump1  12205  fsum00  12247  telfsumo  12251  fsumparts  12255  hashiun  12263  binomlem  12268  binom1dif  12272  bcxmas  12274  isumsplit  12276  isum1p  12277  arisum  12283  arisum2  12284  trireciplem  12285  explecnv  12290  geolim  12296  georeclim  12298  mertenslem2  12321  mertensabs  12322  prodf1f  12328  prodrbdclem2  12358  efcllemp  12443  ef0lem  12445  efgt0  12469  eftlub  12475  efsep  12476  effsumlt  12477  tanval3ap  12499  efi4p  12502  resin4p  12503  recos4p  12504  ef01bndlem  12541  sin01bnd  12542  cos01bnd  12543  sinltxirr  12546  sin01gt0  12547  cos01gt0  12548  absefib  12556  efieq1re  12557  eirraplem  12562  dvdsdc  12583  dvdscmulr  12605  fsumdvds  12627  dvdslelemd  12628  3dvds  12649  odd2np1lem  12657  odd2np1  12658  flodddiv4  12721  bitsfzo  12740  bitsmod  12741  gcdsupex  12752  gcdsupcl  12753  gcd1  12782  nninfctlemfo  12835  nn0seqcvgd  12837  algcvg  12844  algcvgblem  12845  eucalg  12855  prmind2  12916  qden1elz  13003  dfphi2  13020  phiprm  13023  phimullem  13025  prmdiv  13035  prmdiveq  13036  prm23lt5  13064  pcpre1  13093  pczpre  13098  pcdiv  13103  pc1  13106  pcqdiv  13108  pcexp  13110  pcxnn0cl  13111  pcxcl  13112  pcdvdstr  13128  pc2dvds  13131  sumhashdc  13148  fldivp1  13149  pcfaclem  13150  qexpz  13153  expnprm  13154  prmpwdvds  13156  pockthlem  13157  4sqlem5  13183  4sqlem6  13184  4sqlem11  13202  4sqlem13m  13204  4sqlem19  13210  prmlem1a  13243  ballotfilemofi  13270  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemodife  13291  ballotfilemscl  13298  ballotfilemsle  13299  oddennn  13334  xpct  13338  ennnfonelemj0  13343  ennnfonelemen  13363  ctinfomlemom  13369  omctfn  13385  restid  13655  imasbas  13679  imasplusg  13680  imasmulr  13681  imasaddfnlemg  13686  xpscf  13719  gzsumvalx  13760  gzsumsplit1r  13766  gzsumcl  13855  mulgnngzsum  13981  mulgnndir  14005  mulgneg2  14010  gsumvalfi  14203  prdsex  14223  prdsval  14224  prdsbaslemss  14225  prdsbas  14227  prdsgrpd  14248  prdsinvgd  14249  dvdsrmuld  14454  zsssubrg  14973  znval  15022  znle  15023  znbaslemnn  15025  znf1o  15037  znleval  15039  psrval  15101  restuni2  15330  cnrest2r  15390  lmfss  15397  lmres  15401  lmtopcnp  15403  ispsmet  15476  isxmet2d  15501  ismet2  15507  blfvalps  15538  blex  15540  xblss2  15558  reopnap  15699  divcnap  15718  climcncf  15737  cncfmpt2fcntop  15752  hovera  15800  limcdifap  15815  cnplimcim  15820  cnlimcim  15824  cnlimc  15825  cnlimci  15826  dvbss  15838  dvcnp2cntop  15852  dvcn  15853  dvaddxxbr  15854  dvmulxxbr  15855  dvexp  15864  dveflem  15879  plyval  15885  elply2  15888  plyf  15890  plyss  15891  plyssc  15892  elplyr  15893  plyaddlem1  15900  plymullem1  15901  plyaddlem  15902  plymullem  15903  plyco  15912  plycj  15914  dvply1  15918  reeff1olem  15924  sinperlem  15962  sin2kpi  15965  cos2kpi  15966  sin2pim  15967  cos2pim  15968  cosq14gt0  15986  coseq0q4123  15988  tangtx  15992  abssinper  16000  sinkpi  16001  coskpi  16002  cosq34lt1  16004  logrpap0b  16031  logdivlti  16036  rpcxpsqrtth  16088  rpabscxpbnd  16098  binom4  16141  birthdaylem2  16148  birthdaylem3  16149  wilthlem1  16154  0sgm  16176  ppiprm  16181  ppinprm  16182  chtprm  16183  chtnprm  16184  chtdif  16186  ppiqp1le  16189  ppidif  16191  ppiqeq0  16202  ppiqltx  16203  prmorcht  16204  1sgmprm  16210  1sgm2ppw  16211  ppiublem2  16214  ppiqub  16215  chtublem  16217  chtqub  16218  mersenne  16219  perfect1  16220  perfectlem1  16221  perfectlem2  16222  perfect  16223  bcp1ctr  16228  bclbnd  16229  bposlem1  16233  bposlem2  16234  bposlem3  16235  bposlem4  16236  bposlem5  16237  lgslem1  16241  lgsval  16245  lgsfvalg  16246  lgsfcl2  16247  lgsfcl  16249  lgsval2lem  16251  lgsvalmod  16260  lgsneg  16265  lgsdilem  16268  lgsdir2lem3  16271  lgsdir  16276  lgsdilem2  16277  lgsdi  16278  lgsne0  16279  lgsabs1  16280  lgsprme0  16283  lgsdirnn0  16288  lgsdinn0  16289  gausslemma2dlem0d  16293  gausslemma2dlem1a  16299  gausslemma2dlem1f1o  16301  gausslemma2dlem3  16304  gausslemma2dlem4  16305  gausslemma2dlem5a  16306  gausslemma2dlem5  16307  gausslemma2dlem6  16308  lgseisenlem2  16312  lgseisen  16315  lgsquadlem1  16318  lgsquadlem2  16319  lgsquad2lem1  16322  lgsquad2lem2  16323  lgsquad2  16324  m1lgs  16326  2lgslem1  16332  2lgslem2  16333  2lgs  16345  2sqlem9  16365  2sqlem10  16366  ushgredgedg  16589  ushgredgedgloop  16591  uhgrspansubgrlem  16639  wlkvtxiedg  16708  wlkvtxiedgg  16709  wlk1walkdom  16722  upgr2wlkdc  16740  clwwlkccatlem  16763  umgrclwwlkge2  16765  clwwlknonmpo  16791  clwwlknonex2lem2  16801  clwwlknonex2  16802  konigsberglem1  16851  pwle2  17150  pw1nct  17155  nninfsellemdc  17175  nnnninfen  17186  nnnninfex  17187  nninfnfiinf  17188  sbthom  17193  repiecelem  17196  repiecele0  17197  trirec0  17215  apdifflemr  17218  reap0  17230  nconstwlpolem  17237