Theorem syl2an 501

Description: A double syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
syl2an.2	|- (th -> ph)
syl2an.3	|- (ta -> ps)

Assertion

Ref	Expression
syl2an	|- ((th /\ ta) -> ch)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		sylan.1	. . 3 |- ((ph /\ ps) -> ch)
2		syl2an.2	. . 3 |- (th -> ph)
3	1, 2	sylan 495	. 2 |- ((th /\ ps) -> ch)
4		syl2an.3	. 2 |- (ta -> ps)
5	3, 4	sylan2 498	1 |- ((th /\ ta) -> ch)

Syntax hints:   -> wi 3   /\ wa 239

This theorem is referenced by:  ax11indalem 1597  eqeqan12d 1738  sylan9eq 1785  sbccomg 2359  csbcomg 2393  csbnestg 2414  sylan9ss 2461  ssconb 2570  ineqan12d 2626  ifpr 2899  breqan12d 3174  copsex2g 3354  tz7.7 3499  ordin 3504  onin 3505  ontri1 3510  onelpss 3518  onsseleq 3519  ontr2 3526  unexg 3609  eualeq 3634  euexeqOLD 3637  ordon 3674  peano4 3785  findsg 3791  vtoclr 3843  opthprc 3857  xpss12OLD 3901  relop 3924  sotri 4126  unixp 4233  coexg 4240  funco 4268  funcoOLD 4269  funssres 4271  funsnOLD 4275  funtp 4279  fnco 4332  fcoOLD 4385  fodmrnu 4437  resdif 4470  dffv2 4545  eqfnfv 4577  fconst2g 4632  isofrlem 4689  opreqan12d 4713  oprabval5 4769  curry1 4886  curry2 4889  onfununi 4927  tfrlem5 4934  tfrlem11 4940  tz7.48lem 4975  oacan 5040  oawordri 5043  oaass 5054  omord2 5057  omcan 5059  oeord 5074  oecan 5075  oeordsuc 5080  nnasuc 5088  nnmsuc 5089  nnecl 5096  nneclOLD 5097  nnacom 5099  nnaordi 5100  nnaword1 5112  nnmordi 5114  oaabslem 5119  oaabs 5120  omsmo 5125  brecop 5176  ecopoprtrn 5181  th3qlem1 5184  ecoprdi 5191  mapvalg 5200  pmvalg 5201  mapsn 5215  en2sn 5301  sbthlem7 5327  sbth 5331  sdomnsym 5336  domtriord 5357  xpen 5392  mapenlem1 5393  mapenlem2 5394  mapdom1 5396  mapdom2 5398  limenpsi 5409  phplem4 5415  php 5417  php3 5419  nndomo 5424  ominf 5432  pssnn 5438  unblem2 5444  isfinite2 5449  unfilem1 5451  unfilem2 5452  unfi2 5455  unifi2 5459  fodomfi 5466  inf3lem6 5533  rankxplim 5632  cardnn 5666  omsubsuc2 5674  omsubsdom 5677  omsubdom 5678  omsubel 5679  omsubss 5680  aceq5lem4 5696  kmlem6 5728  zorn2lem6 5751  fodom 5756  brdom6disj 5763  carddomi 5782  unxpdomlem 5791  unxpdom2 5793  ondomcard 5805  cdaval 5863  cdafi 5882  nnaun 5885  axrepndlem2 5893  axrepnd 5894  ltsopi 5964  mulclpi 5969  addcompi 5970  mulcompi 5972  distrpi 5974  ltexpi 5977  ltapi 5978  ltmpi 5979  addcmpblnq 6000  mulpipq 6003  addclpq 6006  addasspq 6011  distrpq 6015  ltsopq 6023  ltrpq 6033  genpnnp 6056  mulclprlem 6069  distrlem1pr 6075  distrlem5pr 6079  addcanpr 6100  reclem3pr 6106  mulcmpblnr 6131  addsrpr 6132  mulclsr 6141  mulasssr 6147  distrsr 6148  ltsosr 6151  1idsr 6155  00sr 6156  recexsrlem 6160  mulgt0sr 6162  suppsr3 6172  addcnsr 6201  axmulopr 6214  axmulass 6227  axdistr 6228  ax0id 6230  axcnre 6235  cnegexlem3 6297  cnegex 6298  muladd 6378  muladdOLD 6379  resubcl 6397  addsub4 6436  mulsub 6440  ltxrlt 6465  axltadd 6470  lenlt 6475  ltadd2 6603  leadd2 6605  ltsubadd2 6607  lesubadd2 6609  ltaddsub2 6611  leaddsub2 6613  leltadd 6626  addgtge0OLD 6632  ltaddpos2 6636  posdif 6639  addge02 6658  subge0 6659  suble0 6660  mullt0 6666  recextlem1 6670  recextlem2 6671  recex 6672  divmuldiv 6752  conjmul 6770  prodgt02 6800  prodge02 6802  lemul2 6808  lemul2OLD 6809  lemul1a 6814  lemul1aOLD 6815  lemul2a 6816  lemul2aOLD 6817  ltmulgt12 6824  ltmuldiv2 6842  ltmuldiv2OLD 6843  ltdivmulOLD 6845  ledivmulOLD 6847  ltdivmul2 6848  lt2mul2div 6849  lt2mul2divOLD 6850  ledivmul2 6851  ledivmul2OLD 6852  lemuldiv2 6854  lemuldiv2OLD 6855  lereci 6858  ledivdiv 6868  lediv2 6869  ltdiv23 6870  lediv23 6871  max1 6893  max2 6895  min1 6897  min2 6898  nnaddcl 6918  nnmulcl 6919  nnleltp1 6933  nnltp1le 6934  nnaddm1cl 6937  nndiv 6938  addltmul 7024  rpaddcl 7042  rpmulcl 7043  rpdivcl 7044  reuunineg 7070  nnrecl 7076  supxrbnd1 7099  supxrbnd2 7100  nn0nnaddcl 7130  nn0leltp1 7132  nn0ltlem1 7133  nn0sub 7165  zaddcl 7169  zsubcl 7172  znnsub 7181  znn0sub 7182  zmulcl 7184  zleltp1 7186  nn0lem1lt 7189  nnlem1lt 7190  nnltlem1 7191  zdiv 7192  z2ge 7195  zextle 7196  zextlt 7197  btwnnz 7199  prime 7202  zneo 7207  peano2uz2 7208  uzind 7212  uzindOLD 7215  uzwo4OLD 7217  zmax 7228  rebtwnz 7230  qre 7234  qaddcl 7244  qnegcl 7245  qsubcl 7247  irradd 7252  qbtwnre 7254  qbtwnxr 7255  flge 7267  fllt 7268  flval3 7274  fladdz 7279  flzadd 7280  quoremnn0ALT 7288  quoremnn0 7289  fldiv 7292  modlt 7299  flmulnn0 7303  flmulnn0OLD 7304  modmulnn 7305  zmodcl 7306  modcyc 7311  monoord 7318  elioc2 7353  elico2 7354  elicc2 7355  icoshftf1oii 7373  snunioolem 7378  ioojoin 7380  uzneg 7393  uz11 7396  eluzp1m1 7397  eluzp1p1 7399  uzaddcl 7413  uzwo 7419  uzwoOLD 7420  indstr 7425  elfz1eq 7457  fzn 7458  elfz2nn0 7462  fznn0sub2 7466  fzaddel 7467  fzsubel 7468  fzopth 7469  fzsuc 7473  fzrev2 7485  fzrev3 7487  fzrevral 7493  fzrevral3 7495  fzshftral 7496  fseqsupcl 7499  om2uzlti 7504  om2uzlt2i 7505  om2uzf1oi 7507  ser1add2i 7546  ser1addi 7547  seqzp1 7586  seqzval2 7591  seqzrn2 7594  expp1 7612  expcllem 7613  expadd 7634  expmul 7635  expsub 7636  expsubOLD 7637  expordi 7640  expcan 7641  expord 7642  expwordi 7643  expmwordi 7646  lt2sq 7670  le2sq 7671  bernneq 7693  bernneqOLD 7694  bernneq2 7695  expnbnd 7696  digit2 7699  digit1 7700  sqrlem6 7723  sqrlem12 7729  sqrlei 7752  sqrlti 7753  sqr4 7762  sqr9 7763  sqr2irr 7774  crre 7814  crim 7815  mulre 7822  resub 7851  imsub 7854  cjsub 7861  cjreim 7873  cjreim2 7874  cj11OLD 7876  absreimsq 7902  absreim 7903  sqabs 7915  absdiflt 7930  absdifle 7931  abssuble0 7943  absmax 7944  abs2difabs 7950  seq1bndi 7957  cau2i 7960  cau4ii 7965  cau5i 7966  cvg1i 7967  cvg1 7968  cvg3i 7970  caubndi 7973  caurei 7974  cauimi 7975  ser1absdiflem 7976  ser1absdifi 7977  facdiv 7989  facwordi 7991  faclbnd 7992  faclbnd3 7994  faclbnd4lem4 7998  faclbnd5 8000  faclbnd6 8001  facavg 8002  bcval4 8008  bccmpl 8009  bccl2 8018  fsum1ps 8073  fsumsplit 8075  fsumadd 8077  fsumrev 8084  fsumrev2 8085  fsumshft 8086  fsumshftm 8087  fsumcmp 8095  fsumcmpndx2 8097  fsumabs 8098  fsumabs2mul 8099  binomlem1 8121  binomlem2 8122  binomlem4 8124  binomlem5 8125  clm3i 8134  climshfti 8159  climge0 8167  climaddlem3 8171  climmullem1 8175  climmullem4 8178  climmullem5 8179  climmullem8 8182  climsub 8185  clim2serz 8189  clim2serzi 8200  climserzlei 8202  climcaui 8211  caucvglem5 8216  caucvglem6 8217  caucvgi 8218  serzf0i 8224  ser1cmp2lem 8231  ser1cmp2i 8232  cvgcmp3ci 8242  reccnv 8274  infcvglem1 8277  geoseri 8291  cvgratlem2ALT 8305  cvgratlem1 8307  cvgratlem2 8308  fsum0diaglem2 8314  fsum0diag4 8318  negfcncfi 8326  mulc1cncf 8336  ivthlem6 8343  ivthlem7 8344  ivthlem8 8345  efseq0ex 8368  efaddlem3 8397  efaddlem5 8399  efaddlem6 8400  efaddlem11 8405  efaddlem13 8407  efaddlem14 8408  efaddlem17 8411  efaddlem19 8413  abspef01tlubi 8455  reeff1o 8486  efieq 8510  sinsub 8515  cossub 8516  subsin 8518  addcos 8519  subcos 8520  nn0ennn 8561  xpnnen 8563  znnenlem 8565  znnen 8566  infpnlem1 8570  infpn2 8573  infxpidmlem1 8616  infxpidmlem11 8626  infxpidmlem12 8627  infunabs 8629  infcdaabs 8630  infdif 8632  infxpabs 8634  infmap1 8637  infpss 8638  iunctb 8639  unctb 8641  alephmul 8647  subbas 8709  subtop 8711  retopbas 8720  txuni 8730  neiint 8790  innei 8807  islp2 8818  iscn 8829  iscnp 8831  cnco 8840  cnconst 8852  sncld 8859  metxplem1 8898  metxplem2 8899  metxp 8906  bl2in 8915  opnin 8941  metcnp 8960  metcn 8962  cncfmet 8978  remetdval 8981  bl2ioo 8984  ioo2bl 8985  blssioo 8986  tgioolem 8987  lmuni 9024  caussi 9027  causs 9028  lmle 9033  xplm 9048  xpcn 9049  bcthlem8 9079  bcthlem9 9080  bcthlem18 9089  bcthlem20 9091  bcthlem21 9092  gxnn0suc 9182  gxnn0add 9192  gxadd 9193  gxsub 9194  gxnn0mul 9195  gxmul 9196  gxmodid 9197  abldivdiv4 9212  ablmul 9234  ghgrpilem1 9236  ghsubgi 9241  gacan 9255  vcoprnelem 9324  vacnlem3 9464  sqcn 9469  nmcnilem 9471  sm1cnilem 9481  nvo00 9558  nmoge0 9564  nmorepnf 9565  nmolb 9568  nmoub3i 9570  blocnilem 9599  blocni 9600  cnph 9614  ipasslem1 9626  ipasslem2 9627  ipasslem4 9629  ipasslem8 9633  ipasslem11 9636  ipblnfi 9652  phoeqi 9654  ajval 9658  ubthlem7 9673  ubthlem8 9674  ubthlem9 9675  ubthlem10 9676  ubthlem11 9677  ubthlem12 9678  ubthlem12OLD 9679  ubthlem13 9680  ubthlem13OLD 9681  ubthlem14 9682  minveclem9 9693  minveclem16 9700  minveclem18 9702  minveclem19 9703  minveclem21 9705  minveclem24 9708  minveclem25 9709  minveclem26 9710  minveclem27 9711  minveclem28 9712  minveclem30 9714  minveclem31 9715  minveclem36 9720  minveclem38 9722  minveceu 9723  htthlem6 9767  htthlem8 9769  pilem2 9816  pilem3 9817  pigt2lt4 9819  sincosq1sgn 9848  sincosq2sgn 9849  sincosq3sgn 9850  sincosq4sgn 9851  sinq12gt0t 9852  sincosq1eq 9854  sincos6thpi 9856  cosh111lem1 9863  efgh 9867  efifolem1 9871  efifolem2 9872  efifolem3 9873  efifolem4 9874  efifolem5 9875  efifolem6 9876  efifolem7 9877  efif1lem1 9879  efif1lem3 9881  efif1lem4 9882  eff1i 9893  relogeftb 9914  relogoprlem 9918  relogexp 9923  setwoe 9964  dif1en 9966  cdrci 9975  elghomlem1 9986  tx1cn 10015  tx2cn 10016  upxp 10017  uptx 10018  txcnopab 10020  homeofval 10026  subcld 10046  filmapss 10101  flimff 10109  hvsub4 10330  his7 10381  his2sub2 10384  hial2eq2 10398  normpyc 10438  hhph 10470  bcs2 10474  hcau2 10480  hhssabli 10557  hhssnv 10559  hhsscms 10575  ocorth 10589  chocunii 10597  projlem2 10612  projlem26 10636  projlem28 10638  projlem31 10641  pjtheu2i 10675  pjpj0i 10680  shsel3 10704  shscli 10706  chsupss 10735  shjval 10746  chjval 10747  shjcl 10753  chjcl 10754  shsvsi 10761  shsleji 10763  chslej 10846  chjcom 10854  chub1 10855  chdmj1 10877  spanunsni 10927  spanpr 10928  fh1 10986  fh2 10987  cm2j 10988  osumlem2 11006  osumlem3 11007  spansncvi 11024  5oalem1 11026  5oalem3 11028  5oalem5 11030  3oalem2 11035  pjvi 11077  pjds3i 11085  hoaddcl 11113  hoeq 11115  hoadddi 11158  hoadddir 11159  hosubdi 11163  hosub4 11168  hoeq1 11185  hoeq2 11186  counop 11274  adjeq 11288  brafnmul 11304  lnopsubi 11327  hmops 11374  hmopm 11375  hmopd 11376  hmopco 11377  nmcopexlem1 11380  nmcopexlem3 11382  nmcopexlem5 11384  nmcopexlem6 11385  lnopconi 11392  lnfnsubi 11404  nmcfnexlem1 11409  nmcfnexlem3 11411  nmcfnexlem5 11413  nmcfnexlem6 11414  lnfnconi 11419  nlelshi 11422  riesz3i 11424  riesz1 11427  cnlnadjlem2 11430  cnlnadjlem6 11434  cnlnssadj 11442  adjlnop 11448  adjmul 11454  adjadd 11455  nmopcoi 11457  cnvbramul 11478  kbass2 11480  kbass4 11482  kbass6 11484  leopadd 11495  leopmul2i 11498  leoptri 11499  leopnmid 11501  hmopidmchi 11515  cvcon3 11648  dmdmd 11664  mddmd 11665  ssdmd1 11677  ssdmd2 11678  cvdmd 11701  superpos 11718  chrelati 11728  atcv0eq 11743  atomli 11746  atcvatlem 11749  atcvati 11750  atcvat2i 11751  irredlem4 11757  atcvat3i 11760  atcvat4i 11761  mdsymlem2 11768  mdsymlem3 11769  mdsymlem5 11771  mdsymlem8 11774  dmdsym 11777  cdjreui 11796  cdj1i 11797  cdj3lem2b 11801  cdj3lem3 11802  cdj3lem3b 11804  cdj3i 11805  bnj563 12333  bnj565 12335  bnj924 12625  bnj1116 12720  bnj554 13071  bnj557 13073  bnj569 13079  bnj594 13092  bnj953 13135  bnj1178 13238  lemulge12 13392  fz1eqblem 13400  fzind 13402  fnn0ind 13403  zmodid2 13406  zmodfz 13407  cayleylem2 13434  supminf 13448  nn0seqcvgd 13451  negdvdsb 13463  dvdsnegb 13464  dvdsmul1 13468  dvdsadd 13480  dvdsaddr 13481  dvdssub 13482  dvdssubr 13483  dvdsle 13485  alzdvds 13487  divalglem0 13488  divalglem4 13491  divalglem8 13495  divalglem9 13496  divalgb 13499  divalgmod 13501  ndvdsadd 13503  gcdcllem2 13511  gcdaddm 13527  gcdabs 13529  modgcd 13530  algcvg 13536  algcvga 13539  eucalglt 13545  mulgcdlem3 13550  mulgcdlem7 13554  mulgcd 13555  absmulgcd 13556  isprm2lem 13566  isprm3 13568  coprmdvds 13575  dfon2lem4 13643  tz6.26 13705  frxp 13743  poseq 13746  soseq 13747  wfrlem10 13758  axdenselem4 13812  axdenselem5 13813  axfelem1 13821  uninqs 14068  elo 14070  surrc2 14120  unpde2eg2 14136  infxpg 14152  celsor 14173  injrec 14190  reacomsmgrp1 14426  reacomsmgrp4 14429  osneisi 14596  fgsb 14635  fgsb2 14639  limfillem2 14653  dtt2 14665  altretop 14707  dmse1 14711  trran 14724  cnvtr 14726  1ded 14767  1cat 14788  dualcat2 14815  ismonc 14845  idsubfun 14888  isseg1 14986  dmsdtriordOLD 15042  fictb 15053  omsubsuc2OLD 15069  omsubsdomOLD 15072  omsubdomOLD 15073  omsubelOLD 15074  omsubssOLD 15075  opncldf1 15084  opnregcld 15097  cldregopn 15098  subsubtop 15105  uncomp 15115  connsub 15125  reconn 15133  ivthALT 15136  fclusff 15305  istail 15316  euuni2 15345  prfunOLD 15359  cocanfo 15371  oprabvalg 15388  indexa 15435  frfi 15453  zmodfzcl 15462  fzadd2 15473  fzsplit 15474  fzdisj 15475  fzm1 15478  sdclem2 15492  sdc 15493  incsequz 15497  incsequz2 15498  fsumlt 15503  csbrni 15514  mettrifi2 15530  geomcau 15531  iccshftr 15539  iccshftl 15541  iccdil 15543  icccntr 15545  lincmb01cmp 15560  lincmb01icc 15561  ishomeo2 15578  haustlmu 15588  lmtlm 15590  txsubsp 15594  cnresoprab 15597  txmet 15607  sstotbnd 15618  totbndbnd 15626  ismtyval 15629  isismty 15630  ismtyhmeo 15633  ismtyres 15636  heiborlem12 15648  heiborlem15 15651  heiborlem16 15652  heiborlem26 15662  heiborlem28 15664  heiborlem32 15668  heiborlem33 15669  heiborlem35 15671  heiborlem38 15674  bfplem8 15687  recms 15692  rrnmet 15698  rrndstprj2 15700  rrntotbndlem1 15702  rrntotbndlem2 15703  rrntotbnd 15704  iccbnd 15708  phtpycom 15732  phtpycolem2 15734  reparpht 15747  pcocn 15758  pcohtpylem2 15763  pcohtpy 15765  pcoass 15767  pcorevlem 15768  rnggrphom 15807  prnc 15897  ispridlc 15900  pridlc3 15903  strssp1 16472  strdif 16478  lubel 16655  atomcmp 16757  hlatmstc 16790  cvr1 16795  ps-1 16807  zaddablxNEW 16870  pointpsub 16959  linepsub 16960  pmapsub 16971  pmapglb 16972  paddasslem14 17006  polat 17021

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 163  df-an 241

Copyright terms: Public domain