Theorem syl2an 454

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 448	. 2 |- ((th /\ ps) -> ch)
4		syl2an.3	. 2 |- (ta -> ps)
5	3, 4	sylan2 451	1 |- ((th /\ ta) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ax11indalem 1368  sbccomg 1989  csbcomg 2017  csbnestg 2036  ssconb 2170  ineqan12d 2219  ifpr 2427  breqan12d 2632  copsex2g 2793  unexg 2874  tz7.7 2973  ordin 2977  onin 2978  ontri1 2981  ordon 2987  onelpsst 2998  onsseleq 2999  ontr2 3004  peano4 3152  findsg 3157  vtoclr 3211  opthprc 3221  ssxp 3256  relop 3275  sotri 3443  unixp 3517  coexg 3524  funsn 3543  funco 3550  funssres 3552  fnco 3595  fco 3636  fodmrnu 3680  eqfnfv 3797  fconst2g 3845  isofrlem 3901  tfrlem5 3915  tfrlem11 3921  tz7.48lem 3955  opreqan12d 3979  oprabval5 4029  curry1 4098  oacan 4182  oawordri 4184  oaass 4195  omord2 4198  omcan 4200  oeord 4215  oecan 4216  oeordsuc 4221  nnasuc 4225  nnmsuc 4226  nnecl 4231  nnacom 4233  nnaordi 4234  nnaword1 4244  nnmordi 4246  oaabslem 4251  oaabs 4252  omsmo 4257  brecop 4306  ecopoprtrn 4311  th3qlem1 4314  ecoprdi 4321  mapvalg 4330  pmvalg 4331  mapsn 4345  en2sn 4431  sbthlem7 4453  sbth 4457  sdomnsym 4462  xpen 4488  mapenlem1 4489  mapenlem2 4490  mapdom1 4492  mapdom2 4494  limenpsi 4505  phplem4 4511  php 4513  php3 4515  php3OLD 4516  nndomo 4521  ominfOLD 4529  pssnn 4534  unblem2 4541  isfinite2OLD 4546  unfilem1 4548  unfilem2 4549  unfi2 4553  unifi2 4558  fodomfiOLD 4566  inf3lem6 4618  rankxplim 4712  aceq5lem4 4738  kmlem6 4770  zorn2lem6 4793  fodom 4798  brdom6disj 4805  cardnn 4824  carddomi 4835  unxpdomlem 4843  unxpdom2 4845  ondomcard 4857  cdavalt 4919  cdafi 4936  axrepndlem2 4945  axrepnd 4946  ltsopi 5016  mulclpi 5021  addcompi 5022  mulcompi 5024  distrpi 5026  ltexpi 5029  ltapi 5030  ltmpi 5031  addcmpblnq 5052  mulpipq 5055  addclpq 5058  addasspq 5063  distrpq 5067  ltsopq 5075  ltrpq 5085  genpnnp 5108  mulclprlem 5121  distrlem1pr 5127  distrlem5pr 5131  addcanpr 5152  reclem3pr 5158  mulcmpblnr 5183  addsrpr 5184  mulclsr 5193  mulasssr 5199  distrsr 5200  ltsosr 5203  1idsr 5207  00sr 5208  recexsrlem 5212  mulgt0sr 5214  suppsr3 5224  addcnsr 5253  axmulopr 5266  axmulass 5278  axdistr 5279  ax0id 5281  axcnre 5286  cnegextlem3 5347  cnegext 5348  muladdt 5421  resubclt 5438  addsub4t 5473  mulsubt 5477  ltxrltt 5500  axltadd 5505  lenltt 5510  ltadd2t 5624  leadd2t 5626  ltsubadd2t 5628  lesubadd2t 5630  ltaddsub2t 5632  leaddsub2t 5634  leltaddt 5646  addgtge0t 5649  ltaddpos2t 5652  posdift 5654  addge02t 5673  subge0t 5674  suble0t 5675  recextlem1 5682  recextlem2 5683  recext 5684  divmuldivt 5780  divdivdivt 5785  conjmult 5797  prodgt02t 5827  prodge02t 5829  lemul2t 5833  lemul1it 5837  lemul1itOLD 5838  lemul2it 5839  lemul2itOLD 5840  ltmulgt12t 5847  ltmuldiv2t 5865  ltmuldiv2tOLD 5866  ltdivmultOLD 5868  ledivmultOLD 5869  ltdivmul2t 5870  ltdivmul2tOLD 5871  lt2mul2divt 5872  ledivmul2tOLD 5873  lemuldiv2t 5876  lemuldiv2tOLD 5877  lerec 5880  ledivdivt 5890  lediv2t 5891  max1 5915  max2 5917  min1 5919  min2 5920  nnaddclt 5940  nnmulclt 5941  nnleltp1t 5954  nnltp1let 5955  nnaddm1clt 5958  nndivt 5959  reuunineg 6066  nnreclt 6072  supxrbnd1 6095  supxrbnd2 6096  nn0nnaddclt 6126  nn0leltp1t 6128  nn0ltlem1t 6129  nn0subt 6161  zaddclt 6165  zsubclt 6168  znnsubt 6177  znn0subt 6178  zmulclt 6180  zleltp1t 6182  nn0lem1ltt 6185  nnlem1ltt 6186  nnltlem1t 6187  z2get 6188  zextlet 6189  zextltt 6190  btwnnzt 6192  primet 6195  zneo 6200  peano2uz2 6201  uzind 6205  uzindOLD 6208  uzwo4OLD 6210  zmax 6220  rebtwnz 6222  flget 6233  flltt 6234  flval3t 6239  fladdzt 6244  quoremOLD 6252  qret 6259  qnegclt 6270  qsubclt 6272  qrecclt 6273  qbtwnre 6278  qbtwnxr 6279  rpaddclt 6290  rpmulclt 6291  rpdivclt 6292  monoord 6294  om2uzlt 6298  om2uzlt2 6299  om2uzf1o 6301  ser1add2 6338  ser1add 6339  elioc2t 6390  elico2t 6391  elicc2t 6392  icoshftf1oi 6409  snunioolem 6414  ioojoint 6416  uznegit 6429  uz11t 6432  eluzp1m1t 6433  eluzp1p1t 6435  uzaddclt 6449  uzwo 6455  uzwoOLD 6456  indstr 6461  elfz1eqt 6492  fznt 6493  elfz2nn0t 6495  fznn0sub2t 6499  fzaddelt 6500  fzsubelt 6501  fzoptht 6502  fzrev2t 6512  fzrev3t 6514  fzrevralt 6519  fzrevral3t 6521  fzshftralt 6522  fseqsupcl 6525  seqzp1 6548  seqzval2t 6553  seqzrn2 6556  expp1t 6574  expcllem 6575  expaddt 6596  expmult 6597  expsubt 6598  expordit 6600  expcant 6601  expordt 6602  expwordit 6603  expmwordit 6606  lt2sqt 6630  le2sqt 6631  bernneq 6652  bernneq2 6653  expnbndt 6654  nn0opthlem2 6665  sqrlem6 6678  sqrlem12 6684  sqrle 6707  sqrlt 6708  sqr4 6717  sqr9 6718  sqr2irr 6729  crret 6769  crimt 6770  resubt 6806  imsubt 6809  cjsubt 6816  cjreimt 6828  cjreim2t 6829  cj11t 6830  absreimsqt 6856  absreimt 6857  absdifltt 6883  absdiflet 6884  abssuble0t 6896  absmaxt 6897  abs2difabst 6903  seq1bnd 6910  cau2 6913  cau4i 6918  cau5 6919  cvg1i 6920  cvg1 6921  cvg3 6923  caubnd 6926  caure 6927  cauim 6928  ser1absdiflem 6929  ser1absdif 6930  facdivt 6942  facwordit 6944  faclbnd 6945  faclbnd3 6947  faclbnd4lem4 6951  faclbnd5 6953  faclbnd6 6954  facavgt 6955  bcval4t 6961  bccmplt 6962  bccl2t 6971  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  fsumrev 7029  fsumrev2 7030  fsumshft 7031  fsumshftm 7032  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  fsumabs2mul 7044  binomlem1 7066  binomlem2 7067  binomlem4 7069  binomlem5 7070  clm3 7079  climshft 7104  climge0 7112  climaddlem3 7116  climmullem1 7120  climmullem5 7124  climmullem8 7127  climsub 7130  clim2serzt 7134  clim2serz 7145  climserzle 7147  climcau 7156  caucvglem5 7161  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  ser1cmp2lem 7176  ser1cmp2 7177  cvgcmp3c 7186  reccnv 7218  infcvglem1 7221  geoser 7234  cvgratlem2ALT 7248  cvgratlem1 7250  cvgratlem2 7251  fsum0diaglem2 7257  fsum0diag4 7261  negfcncf 7269  mulc1cncf 7279  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  efseq0ex 7311  efaddlem3 7340  efaddlem5 7342  efaddlem6 7343  efaddlem11 7348  efaddlem13 7350  efaddlem14 7351  efaddlem17 7354  efaddlem19 7356  abspef01tlub 7395  reeff1o 7426  efieq 7450  sinsubt 7455  cossubt 7456  subsint 7458  addcost 7459  subcost 7460  nn0ennn 7497  xpnnen 7499  znnenlem 7501  znnen 7502  infpnlem1 7506  infpn2 7509  infxpidmlem1 7552  infxpidmlem11 7562  infxpidmlem12 7563  infunabs 7565  infcdaabs 7566  infdif 7568  infxpabs 7570  infmap1 7573  infpss 7574  iunctb 7575  unctb 7577  alephmul 7583  subbasOLD 7644  subtop 7646  retopbas 7655  neiint 7719  innei 7736  islp2 7747  iscn 7758  iscnp 7760  cnco 7768  cnconst 7780  sncld 7787  metxplem1 7826  metxplem2 7827  metxp 7834  bl2in 7843  opnin 7869  metcnp 7887  metcn 7889  cncfmet 7905  remetdval 7908  bl2ioo 7911  ioo2bl 7912  blssioo 7913  tgioolem 7914  lmuni 7951  caussi 7954  causs 7955  lmle 7960  xplm 7975  xpcn 7976  bcthlem8 8006  bcthlem9 8007  bcthlem18 8016  bcthlem20 8018  bcthlem21 8019  abldivdiv4 8109  ablmul 8131  ghgrpilem1 8133  ghsubgi 8138  vcoprnelem 8197  sqcn 8335  nmcnilem 8337  sm1cnilem 8347  nvo00 8424  nmoge0 8430  nmorepnf 8431  nmolb 8434  nmoub3i 8436  blocnilem 8464  blocni 8465  cnph 8478  ipasslem1 8490  ipasslem2 8491  ipasslem4 8493  ipasslem8 8497  ipasslem11 8500  ipblnfi 8516  phoeqi 8518  ubthlem7 8535  ubthlem8 8536  ubthlem9 8537  ubthlem10 8538  ubthlem11 8539  ubthlem12 8540  ubthlem13 8541  ubthlem14 8542  minveclem9 8553  minveclem16 8560  minveclem18 8562  minveclem19 8563  minveclem21 8565  minveclem24 8568  minveclem25 8569  minveclem26 8570  minveclem27 8571  minveclem28 8572  minveclem30 8574  minveclem31 8575  minveclem36 8580  minveclem38 8582  minveceu 8583  htthlem6 8625  htthlem8 8627  pilem2 8672  pilem3 8673  pigt2lt4 8675  sincosq1sgn 8704  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  sinq12gt0t 8708  sincosq1eq 8709  sincos6thpi 8711  cosh111lem1 8714  efgh 8718  efifolem1 8722  efifolem2 8723  efifolem3 8724  efifolem4 8725  efifolem5 8726  efifolem6 8727  efifolem7 8728  efif1lem1 8730  efif1lem3 8732  efif1lem4 8733  eff1i 8744  relogeftb 8765  relogoprlem 8769  relogexpt 8774  hvsub4t 8906  his7t 8956  his2sub2t 8959  hial2eq2t 8973  normpyct 9013  hhph 9045  bcs2t 9049  hcau2 9055  hhssabl 9132  hhssnv 9134  hhsscms 9150  ocorth 9164  chocuni 9172  projlem2 9187  projlem26 9211  projlem28 9213  projlem31 9216  pjtheu2 9250  pjpj0 9255  shsel3t 9279  shscl 9281  chsupss 9310  shjvalt 9321  chjvalt 9322  shjclt 9328  chjclt 9329  shsvs 9336  shslej 9338  chslejt 9421  chjcomt 9429  chub1t 9430  chdmj1t 9452  spanunsn 9502  spanpr 9503  fh1t 9561  fh2t 9562  cm2jt 9563  osumlem2 9579  osumlem3 9580  spansncv 9597  5oalem1 9599  5oalem3 9601  5oalem5 9603  3oalem2 9608  pjv 9650  pjds3 9658  hoaddclt 9684  hoeqt 9686  hoadddit 9729  hoadddirt 9730  hosubdit 9734  hosub4t 9739  hoeq1t 9756  hoeq2t 9757  counopt 9845  adjeqt 9859  brafnmult 9875  lnopsub 9898  hmopst 9945  hmopmt 9946  hmopdt 9947  hmopcot 9948  nmcopexlem1 9951  nmcopexlem3 9953  nmcopexlem5 9955  nmcopexlem6 9956  lnopcon 9963  lnfnsub 9975  nmcfnexlem1 9980  nmcfnexlem3 9982  nmcfnexlem5 9984  nmcfnexlem6 9985  lnfncon 9990  nlelsh 9993  riesz3 9995  riesz1t 9998  cnlnadjlem2 10001  cnlnadjlem6 10005  cnlnssadj 10013  adjlnopt 10019  adjmult 10025  adjaddt 10026  nmopco 10028  cnvbramult 10048  kbass2t 10050  kbass4t 10052  kbass6t 10054  leopaddt 10065  leopmul2it 10068  leoptrit 10069  leopnmidt 10071  hmopidmch 10079  cvcon3t 10211  dmdmdt 10227  mddmdt 10228  ssdmd1 10240  ssdmd2 10241  cvdmdt 10264  superpos 10281  chrelat 10291  atcv0eq 10306  atoml 10309  atcvatlem 10312  atcvat 10313  atcvat2 10314  irredlem4 10320  atcvat3 10323  atcvat4 10324  mdsymlem2 10331  mdsymlem3 10332  mdsymlem5 10334  mdsymlem8 10337  dmdsymt 10340  cdjreu 10359  cdj1 10360  cdj3lem2b 10364  cdj3lem3 10365  cdj3lem3b 10367  cdj3 10368  elghomlem1 10382  cayleylem2 10410  uninqs 10441  elo 10444  cdrci 10494  homeofval 10516  setwoe 10546  fgsb 10570  fgsbOLD 10571  fgsb2 10580  dtt2 10618  dmse1 10623  trran 10636  cnvtr 10638  1ded 10671  1cat 10692  ismonc 10742

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 147  df-an 225

Copyright terms: Public domain