Theorem syl2an 456

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ax11indalem 1370  sbccomg 1993  csbcomg 2021  csbnestg 2040  ssconb 2174  ineqan12d 2223  ifpr 2432  breqan12d 2638  copsex2g 2800  unexg 2881  tz7.7 2980  ordin 2984  onin 2985  ontri1 2988  ordon 2994  onelpsst 3005  onsseleq 3006  ontr2 3011  peano4 3159  findsg 3164  vtoclr 3218  opthprc 3228  ssxp 3263  relop 3282  sotri 3450  unixp 3524  coexg 3531  funsn 3550  funco 3557  funssres 3559  fnco 3602  fco 3643  fodmrnu 3687  eqfnfv 3804  fconst2g 3852  isofrlem 3908  tfrlem5 3922  tfrlem11 3928  tz7.48lem 3962  opreqan12d 3986  oprabval5 4036  curry1 4105  oacan 4189  oawordri 4191  oaass 4202  omord2 4205  omcan 4207  oeord 4222  oecan 4223  oeordsuc 4228  nnasuc 4232  nnmsuc 4233  nnecl 4238  nnacom 4240  nnaordi 4241  nnaword1 4251  nnmordi 4253  oaabslem 4258  oaabs 4259  omsmo 4264  brecop 4313  ecopoprtrn 4318  th3qlem1 4321  ecoprdi 4328  mapvalg 4337  pmvalg 4338  mapsn 4352  en2sn 4438  sbthlem7 4460  sbth 4464  sdomnsym 4469  xpen 4495  mapenlem1 4496  mapenlem2 4497  mapdom1 4499  mapdom2 4501  limenpsi 4512  phplem4 4518  php 4520  php3 4522  php3OLD 4523  nndomo 4528  ominf 4538  ominfOLD 4539  pssnn 4546  unblem2 4554  isfinite2 4559  isfinite2OLD 4560  unfilem1 4562  unfilem2 4563  unfi2 4567  unfi2OLD 4568  unifi2 4573  unifi2OLD 4575  fodomfi 4582  fodomfiOLD 4583  inf3lem6 4634  rankxplim 4729  aceq5lem4 4755  kmlem6 4787  zorn2lem6 4810  fodom 4815  brdom6disj 4822  cardnn 4841  carddomi 4852  unxpdomlem 4861  unxpdom2 4863  ondomcard 4875  cdavalt 4938  cdafi 4955  axrepndlem2 4964  axrepnd 4965  ltsopi 5035  mulclpi 5040  addcompi 5041  mulcompi 5043  distrpi 5045  ltexpi 5048  ltapi 5049  ltmpi 5050  addcmpblnq 5071  mulpipq 5074  addclpq 5077  addasspq 5082  distrpq 5086  ltsopq 5094  ltrpq 5104  genpnnp 5127  mulclprlem 5140  distrlem1pr 5146  distrlem5pr 5150  addcanpr 5171  reclem3pr 5177  mulcmpblnr 5202  addsrpr 5203  mulclsr 5212  mulasssr 5218  distrsr 5219  ltsosr 5222  1idsr 5226  00sr 5227  recexsrlem 5231  mulgt0sr 5233  suppsr3 5243  addcnsr 5272  axmulopr 5285  axmulass 5297  axdistr 5298  ax0id 5300  axcnre 5305  cnegextlem3 5366  cnegext 5367  muladdt 5440  resubclt 5457  addsub4t 5492  mulsubt 5496  ltxrltt 5519  axltadd 5524  lenltt 5529  ltadd2t 5643  leadd2t 5645  ltsubadd2t 5647  lesubadd2t 5649  ltaddsub2t 5651  leaddsub2t 5653  leltaddt 5665  addgtge0t 5668  ltaddpos2t 5671  posdift 5673  addge02t 5692  subge0t 5693  suble0t 5694  recextlem1 5701  recextlem2 5702  recext 5703  divmuldivt 5789  divdivdivt 5794  conjmult 5806  prodgt02t 5836  prodge02t 5838  lemul2t 5842  lemul1it 5846  lemul1itOLD 5847  lemul2it 5848  lemul2itOLD 5849  ltmulgt12t 5856  ltmuldiv2t 5874  ltmuldiv2tOLD 5875  ltdivmultOLD 5877  ledivmultOLD 5878  ltdivmul2t 5879  ltdivmul2tOLD 5880  lt2mul2divt 5881  ledivmul2tOLD 5882  lemuldiv2t 5885  lemuldiv2tOLD 5886  lerec 5889  ledivdivt 5899  lediv2t 5900  max1 5924  max2 5926  min1 5928  min2 5929  nnaddclt 5949  nnmulclt 5950  nnleltp1t 5963  nnltp1let 5964  nnaddm1clt 5967  nndivt 5968  reuunineg 6075  nnreclt 6081  supxrbnd1 6104  supxrbnd2 6105  nn0nnaddclt 6135  nn0leltp1t 6137  nn0ltlem1t 6138  nn0subt 6170  zaddclt 6174  zsubclt 6177  znnsubt 6186  znn0subt 6187  zmulclt 6189  zleltp1t 6191  nn0lem1ltt 6194  nnlem1ltt 6195  nnltlem1t 6196  z2get 6197  zextlet 6198  zextltt 6199  btwnnzt 6201  primet 6204  zneo 6209  peano2uz2 6210  uzind 6214  uzindOLD 6217  uzwo4OLD 6219  zmax 6229  rebtwnz 6231  flget 6242  flltt 6243  flval3t 6248  fladdzt 6253  fldivt 6263  qret 6267  qnegclt 6278  qsubclt 6280  qrecclt 6281  qbtwnre 6286  qbtwnxr 6287  rpaddclt 6298  rpmulclt 6299  rpdivclt 6300  monoord 6302  om2uzlt 6306  om2uzlt2 6307  om2uzf1o 6309  ser1add2 6346  ser1add 6347  elioc2t 6398  elico2t 6399  elicc2t 6400  icoshftf1oi 6417  snunioolem 6422  ioojoint 6424  uznegit 6437  uz11t 6440  eluzp1m1t 6441  eluzp1p1t 6443  uzaddclt 6457  uzwo 6463  uzwoOLD 6464  indstr 6469  elfz1eqt 6500  fznt 6501  elfz2nn0t 6503  fznn0sub2t 6507  fzaddelt 6508  fzsubelt 6509  fzoptht 6510  fzrev2t 6520  fzrev3t 6522  fzrevralt 6527  fzrevral3t 6529  fzshftralt 6530  fseqsupcl 6533  seqzp1 6556  seqzval2t 6561  seqzrn2 6564  expp1t 6582  expcllem 6583  expaddt 6604  expmult 6605  expsubt 6606  expordit 6608  expcant 6609  expordt 6610  expwordit 6611  expmwordit 6614  lt2sqt 6638  le2sqt 6639  bernneq 6660  bernneq2 6661  expnbndt 6662  nn0opthlem2 6673  sqrlem6 6686  sqrlem12 6692  sqrle 6715  sqrlt 6716  sqr4 6725  sqr9 6726  sqr2irr 6737  crret 6777  crimt 6778  resubt 6813  imsubt 6816  cjsubt 6823  cjreimt 6835  cjreim2t 6836  cj11t 6837  absreimsqt 6863  absreimt 6864  absdifltt 6890  absdiflet 6891  abssuble0t 6903  absmaxt 6904  abs2difabst 6910  seq1bnd 6917  cau2 6920  cau4i 6925  cau5 6926  cvg1i 6927  cvg1 6928  cvg3 6930  caubnd 6933  caure 6934  cauim 6935  ser1absdiflem 6936  ser1absdif 6937  facdivt 6949  facwordit 6951  faclbnd 6952  faclbnd3 6954  faclbnd4lem4 6958  faclbnd5 6960  faclbnd6 6961  facavgt 6962  bcval4t 6968  bccmplt 6969  bccl2t 6978  fsum1ps 7025  fsumsplit 7027  fsumadd 7029  fsumrev 7036  fsumrev2 7037  fsumshft 7038  fsumshftm 7039  fsumcmp 7047  fsumcmpndx2 7049  fsumabs 7050  fsumabs2mul 7051  binomlem1 7073  binomlem2 7074  binomlem4 7076  binomlem5 7077  clm3 7086  climshft 7111  climge0 7119  climaddlem3 7123  climmullem1 7127  climmullem5 7131  climmullem8 7134  climsub 7137  clim2serzt 7141  clim2serz 7152  climserzle 7154  climcau 7163  caucvglem5 7168  caucvglem6 7169  caucvg 7170  serzf0 7176  ser1f0 7177  ser1cmp2lem 7183  ser1cmp2 7184  cvgcmp3c 7193  reccnv 7225  infcvglem1 7228  geoser 7241  cvgratlem2ALT 7255  cvgratlem1 7257  cvgratlem2 7258  fsum0diaglem2 7264  fsum0diag4 7268  negfcncf 7276  mulc1cncf 7286  ivthlem6 7293  ivthlem7 7294  ivthlem8 7295  efseq0ex 7318  efaddlem3 7347  efaddlem5 7349  efaddlem6 7350  efaddlem11 7355  efaddlem13 7357  efaddlem14 7358  efaddlem17 7361  efaddlem19 7363  abspef01tlub 7402  reeff1o 7433  efieq 7457  sinsubt 7462  cossubt 7463  subsint 7465  addcost 7466  subcost 7467  nn0ennn 7505  xpnnen 7507  znnenlem 7509  znnen 7510  infpnlem1 7514  infpn2 7517  infxpidmlem1 7560  infxpidmlem11 7570  infxpidmlem12 7571  infunabs 7573  infcdaabs 7574  infdif 7576  infxpabs 7578  infmap1 7581  infpss 7582  iunctb 7583  unctb 7585  unctbOLD 7586  alephmul 7592  subtop 7650  retopbas 7659  neiint 7723  innei 7740  islp2 7751  iscn 7762  iscnp 7764  cnco 7772  cnconst 7784  sncld 7791  metxplem1 7830  metxplem2 7831  metxp 7838  bl2in 7847  opnin 7873  metcnp 7891  metcn 7893  cncfmet 7909  remetdval 7912  bl2ioo 7915  ioo2bl 7916  blssioo 7917  tgioolem 7918  lmuni 7955  caussi 7958  causs 7959  lmle 7964  xplm 7979  xpcn 7980  bcthlem8 8010  bcthlem9 8011  bcthlem18 8020  bcthlem20 8022  bcthlem21 8023  abldivdiv4 8112  ablmul 8134  ghgrpilem1 8136  ghsubgi 8141  vcoprnelem 8200  sqcn 8338  nmcnilem 8340  sm1cnilem 8350  nvo00 8427  nmoge0 8433  nmorepnf 8434  nmolb 8437  nmoub3i 8439  blocnilem 8467  blocni 8468  cnph 8481  ipasslem1 8493  ipasslem2 8494  ipasslem4 8496  ipasslem8 8500  ipasslem11 8503  ipblnfi 8519  phoeqi 8521  ubthlem7 8538  ubthlem8 8539  ubthlem9 8540  ubthlem10 8541  ubthlem11 8542  ubthlem12 8543  ubthlem13 8544  ubthlem14 8545  minveclem9 8556  minveclem16 8563  minveclem18 8565  minveclem19 8566  minveclem21 8568  minveclem24 8571  minveclem25 8572  minveclem26 8573  minveclem27 8574  minveclem28 8575  minveclem30 8577  minveclem31 8578  minveclem36 8583  minveclem38 8585  minveceu 8586  htthlem6 8628  htthlem8 8630  pilem2 8674  pilem3 8675  pigt2lt4 8677  sincosq1sgn 8706  sincosq2sgn 8707  sincosq3sgn 8708  sincosq4sgn 8709  sinq12gt0t 8710  sincosq1eq 8711  sincos6thpi 8713  cosh111lem1 8716  efgh 8720  efifolem1 8724  efifolem2 8725  efifolem3 8726  efifolem4 8727  efifolem5 8728  efifolem6 8729  efifolem7 8730  efif1lem1 8732  efif1lem3 8734  efif1lem4 8735  eff1i 8746  relogeftb 8767  relogoprlem 8771  relogexpt 8776  hvsub4t 8908  his7t 8958  his2sub2t 8961  hial2eq2t 8975  normpyct 9015  hhph 9047  bcs2t 9051  hcau2 9057  hhssabl 9134  hhssnv 9136  hhsscms 9152  ocorth 9166  chocuni 9174  projlem2 9189  projlem26 9213  projlem28 9215  projlem31 9218  pjtheu2 9252  pjpj0 9257  shsel3t 9281  shscl 9283  chsupss 9312  shjvalt 9323  chjvalt 9324  shjclt 9330  chjclt 9331  shsvs 9338  shslej 9340  chslejt 9423  chjcomt 9431  chub1t 9432  chdmj1t 9454  spanunsn 9504  spanpr 9505  fh1t 9563  fh2t 9564  cm2jt 9565  osumlem2 9581  osumlem3 9582  spansncv 9599  5oalem1 9601  5oalem3 9603  5oalem5 9605  3oalem2 9610  pjv 9652  pjds3 9660  hoaddclt 9686  hoeqt 9688  hoadddit 9731  hoadddirt 9732  hosubdit 9736  hosub4t 9741  hoeq1t 9758  hoeq2t 9759  counopt 9847  adjeqt 9861  brafnmult 9877  lnopsub 9900  hmopst 9947  hmopmt 9948  hmopdt 9949  hmopcot 9950  nmcopexlem1 9953  nmcopexlem3 9955  nmcopexlem5 9957  nmcopexlem6 9958  lnopcon 9965  lnfnsub 9977  nmcfnexlem1 9982  nmcfnexlem3 9984  nmcfnexlem5 9986  nmcfnexlem6 9987  lnfncon 9992  nlelsh 9995  riesz3 9997  riesz1t 10000  cnlnadjlem2 10003  cnlnadjlem6 10007  cnlnssadj 10015  adjlnopt 10021  adjmult 10027  adjaddt 10028  nmopco 10030  cnvbramult 10050  kbass2t 10052  kbass4t 10054  kbass6t 10056  leopaddt 10067  leopmul2it 10070  leoptrit 10071  leopnmidt 10073  hmopidmch 10081  cvcon3t 10214  dmdmdt 10230  mddmdt 10231  ssdmd1 10243  ssdmd2 10244  cvdmdt 10267  superpos 10284  chrelat 10294  atcv0eq 10309  atoml 10312  atcvatlem 10315  atcvat 10316  atcvat2 10317  irredlem4 10323  atcvat3 10326  atcvat4 10327  mdsymlem2 10334  mdsymlem3 10335  mdsymlem5 10337  mdsymlem8 10340  dmdsymt 10343  cdjreu 10362  cdj1 10363  cdj3lem2b 10367  cdj3lem3 10368  cdj3lem3b 10370  cdj3 10371  elghomlem1 10385  cayleylem2 10413  uninqs 10444  elo 10447  cdrci 10488  homeofval 10510  unpde2eg2 10538  setwoe 10540  fgsb 10563  fgsb2 10568  dtt2 10597  dmse1 10602  trran 10615  cnvtr 10617  1ded 10650  1cat 10671  ismonc 10721

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