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 1345  sbccomg 1960  csbcomg 1988  csbnestg 2007  ssconb 2141  ineqan12d 2190  ifpr 2398  breqan12d 2600  copsex2g 2760  unexg 2838  tz7.7 2936  ordin 2940  onin 2941  ontri1 2944  ordon 2950  onelpsst 2961  onsseleq 2962  ontr2 2967  peano4 3115  findsg 3120  vtoclr 3173  opthprc 3183  ssxp 3218  sotri 3392  unixp 3458  coexg 3465  funsn 3484  funco 3490  funssres 3492  fnco 3535  fco 3575  fodmrnu 3619  eqfnfv 3736  fconst2g 3784  isofrlem 3840  tfrlem5 3854  tfrlem11 3860  tz7.48lem 3894  opreqan12d 3918  oprabval5 3968  curry1 4036  oacan 4120  oawordri 4122  oaass 4133  omord2 4136  omcan 4138  oeord 4153  oecan 4154  oeordsuc 4159  nnasuc 4163  nnmsuc 4164  nnecl 4169  nnacom 4171  nnaordi 4172  nnaword1 4182  nnmordi 4184  oaabslem 4189  oaabs 4190  omsmo 4195  brecop 4244  ecopoprtrn 4249  th3qlem1 4252  ecoprdi 4259  mapvalg 4268  pmvalg 4269  mapsn 4283  en2sn 4366  sbthlem7 4387  sbth 4391  sdomnsym 4396  xpen 4420  mapenlem1 4421  mapenlem2 4422  mapdom1 4424  mapdom2 4426  limenpsi 4437  phplem4 4443  php 4445  php3 4447  nndomo 4452  ominf 4460  pssnn 4465  unblem2 4470  isfinite2 4475  unfilem1 4476  unfilem2 4477  unfi2 4481  unifi2 4485  fodomfi 4492  inf3lem6 4542  rankxplim 4636  aceq5lem4 4662  kmlem6 4694  zorn2lem6 4717  fodom 4722  brdom6disj 4729  cardnn 4748  carddomi 4758  unxpdomlem 4766  unxpdom2 4768  ondomcard 4780  cdavalt 4842  cdafi 4859  axrepndlem2 4868  axrepnd 4869  ltsopi 4939  mulclpi 4944  addcompi 4945  mulcompi 4947  distrpi 4949  ltexpi 4952  ltapi 4953  ltmpi 4954  addcmpblnq 4975  mulpipq 4978  addclpq 4981  addasspq 4986  distrpq 4990  ltsopq 4998  ltrpq 5008  genpnnp 5031  mulclprlem 5044  distrlem1pr 5050  distrlem5pr 5054  addcanpr 5075  reclem3pr 5081  mulcmpblnr 5106  addsrpr 5107  mulclsr 5116  mulasssr 5122  distrsr 5123  ltsosr 5126  1idsr 5130  00sr 5131  recexsrlem 5135  mulgt0sr 5137  suppsr3 5147  addcnsr 5176  axmulopr 5189  axmulass 5201  axdistr 5202  ax0id 5204  axcnre 5209  cnegextlem3 5270  cnegext 5271  muladdt 5344  resubclt 5361  addsub4t 5396  mulsubt 5400  ltxrltt 5423  axltadd 5428  lenltt 5433  ltadd2t 5549  leadd2t 5551  ltsubadd2t 5553  lesubadd2t 5555  ltaddsub2t 5557  leaddsub2t 5559  addgtge0t 5573  ltaddpos2t 5576  posdift 5578  addge02t 5597  subge0t 5598  suble0t 5599  recextlem1 5606  recextlem2 5607  recext 5608  divmuldivt 5687  divdivdivt 5692  conjmult 5704  prodgt02t 5734  prodge02t 5736  lemul2t 5740  lemul1it 5744  lemul1itOLD 5745  lemul2it 5746  lemul2itOLD 5747  ltmulgt12t 5754  ltmuldiv2t 5769  ltdivmult 5770  ledivmult 5771  ltdivmul2t 5772  lt2mul2divt 5773  ledivmul2t 5774  lemuldiv2t 5776  lerec 5779  ledivdivt 5789  lediv2t 5790  max1 5814  max2 5816  min1 5818  min2 5819  nnaddclt 5839  nnmulclt 5840  nnleltp1t 5852  nnltp1let 5853  nnaddm1clt 5856  nndivt 5857  reuunineg 5964  nnreclt 5970  supxrbnd1 5993  supxrbnd2 5994  nn0nnaddclt 6024  nn0leltp1t 6026  nn0ltlem1t 6027  nn0subt 6059  zaddclt 6063  zsubclt 6066  znnsubt 6075  znn0subt 6076  zmulclt 6078  zleltp1t 6080  nn0lem1ltt 6083  nnlem1ltt 6084  nnltlem1t 6085  z2get 6086  zextlet 6087  zextltt 6088  btwnnzt 6090  primet 6093  zneo 6098  zneoOLD 6099  peano2uz2 6100  uzind 6104  uzindOLD 6107  uzwo4OLD 6109  zmax 6119  rebtwnz 6121  flget 6129  flltt 6130  flval3t 6133  fladdzt 6138  qret 6148  qnegclt 6159  qsubclt 6161  qrecclt 6162  qbtwnre 6167  qbtwnxr 6168  rpaddclt 6178  rpmulclt 6179  rpdivclt 6180  monoord 6182  om2uzlt 6186  om2uzlt2 6187  om2uzf1o 6189  ser1add2 6226  ser1add 6227  elioc2t 6273  elico2t 6274  elicc2t 6275  ioonegt 6290  icoshftf1oi 6293  snunioolem 6298  uznegit 6312  uz11t 6315  eluzp1m1t 6316  eluzp1p1t 6318  uzaddclt 6332  uzwo 6338  uzwoOLD 6339  indstr 6344  elfz1eqt 6375  fznt 6376  elfz2nn0t 6378  fznn0sub2t 6382  fzaddelt 6383  fzsubelt 6384  fzoptht 6385  fzrev2t 6395  fzrev3t 6397  fzrevralt 6402  fzrevral3t 6404  fzshftralt 6405  fseqsupcl 6408  seqzp1 6431  seqzval2t 6436  seqzrn2 6439  expp1t 6457  expcllem 6458  expaddt 6478  expmult 6479  expsubt 6480  expordit 6482  expcant 6483  expordt 6484  expwordit 6485  expmwordit 6488  lt2sqt 6512  le2sqt 6513  bernneq 6534  bernneq2 6535  expnbndt 6536  nn0opthlem2 6546  sqrlem6 6559  sqrlem12 6565  sqrle 6588  sqrlt 6589  sqr4 6598  sqr9 6599  sqr2irr 6610  crret 6653  crretOLD 6654  crimt 6655  crimtOLD 6656  resubt 6692  imsubt 6695  cjsubt 6702  cjreimt 6714  cjreim2t 6715  cj11t 6716  absreimsqt 6742  absreimt 6743  absdifltt 6772  absdiflet 6773  abssuble0t 6785  abs2difabst 6791  seq1bnd 6798  cau2 6801  cau4i 6806  cau5 6807  cvg1i 6808  cvg1 6809  cvg3 6811  caubnd 6814  caure 6815  cauim 6816  ser1absdiflem 6817  ser1absdif 6818  facdivt 6830  facwordit 6832  faclbnd 6833  faclbnd3 6835  faclbnd4lem4 6839  faclbnd5 6841  faclbnd6 6842  facavgt 6843  bcval4t 6850  bccmplt 6851  bccl2t 6860  fsum1ps 6907  fsumsplit 6909  fsumadd 6911  fsumrev 6918  fsumrev2 6919  fsumshft 6920  fsumshftm 6921  fsumcmp 6929  fsumcmpndx2 6931  fsumabs 6932  fsumabs2mul 6933  binomlem1 6955  binomlem2 6956  binomlem4 6958  binomlem5 6959  clm3 6968  climshft 6992  climge0 7000  climaddlem3 7003  climmullem1 7007  climmullem5 7011  climmullem8 7014  climsub 7017  clim2serzt 7021  clim2serz 7032  climserzle 7034  climcau 7043  caucvglem5 7048  caucvglem6 7049  caucvg 7050  serzf0 7056  ser1f0 7057  ser1cmp2lem 7063  ser1cmp2 7064  cvgcmp3c 7073  reccnv 7104  infcvglem1 7107  geoser 7120  cvgratlem2ALT 7134  cvgratlem1 7136  cvgratlem2 7137  fsum0diaglem2 7143  fsum0diag4 7147  negfcncf 7155  mulc1cncf 7165  ivthlem6 7172  ivthlem7 7173  ivthlem8 7174  ivthlem6OLD 7181  ivthlem7OLD 7182  efseq0ex 7204  efaddlem3 7233  efaddlem5 7235  efaddlem6 7236  efaddlem11 7241  efaddlem13 7243  efaddlem14 7244  efaddlem17 7247  efaddlem19 7249  abspef01tlub 7287  reeff1o 7319  efieq 7343  sinsubt 7348  cossubt 7349  subsint 7351  addcost 7352  subcost 7353  nn0ennn 7390  xpnnen 7392  znnenlem 7394  znnenlemOLD 7395  znnen 7396  infpnlem1 7400  infpn2 7403  infxpidmlem1 7446  infxpidmlem11 7456  infxpidmlem12 7457  infunabs 7459  infcdaabs 7460  infdif 7462  infxpabs 7464  infmap1 7467  iunctb 7468  unctb 7470  alephmul 7476  subbas 7537  subtop 7539  retopbas 7548  neiint 7608  innei 7625  islp2 7636  iscn 7646  iscnp 7648  cnco 7655  cnconst 7667  sncld 7674  metxplem1 7714  metxplem2 7715  metxp 7722  bl2in 7731  opnin 7757  metcnp 7774  metcn 7776  cncfmet 7792  remetdval 7795  bl2ioo 7798  ioo2bl 7799  blssioo 7800  tgioolem 7801  lmuni 7834  caussi 7837  causs 7838  lmle 7843  xplm 7857  xpcn 7858  bcthlem8 7888  bcthlem9 7889  bcthlem18 7898  bcthlem20 7900  bcthlem21 7901  resgrprnOLD 7979  abldivdiv4 7994  ablmul 8016  ghgrpilem1 8018  ghsubgi 8023  sqcn 8207  nmcnilem 8209  sm1cnilem 8216  nvo00 8291  nmoge0 8297  nmorepnf 8298  nmolb 8301  nmoub3i 8303  blocnilem 8330  blocni 8331  cnph 8344  ipasslem1 8356  ipasslem2 8357  ipasslem4 8359  ipasslem8 8363  ipasslem11 8366  ipblnfi 8382  phoeqi 8384  ubthlem7 8401  ubthlem8 8402  ubthlem9 8403  ubthlem10 8404  ubthlem11 8405  ubthlem12 8406  ubthlem13 8407  ubthlem14 8408  minveclem9 8419  minveclem16 8426  minveclem18 8428  minveclem19 8429  minveclem21 8431  minveclem24 8434  minveclem25 8435  minveclem26 8436  minveclem27 8437  minveclem28 8438  minveclem30 8440  minveclem31 8441  minveclem36 8446  minveclem38 8448  minveceu 8449  htthlem6 8489  htthlem8 8491  pilem2 8504  pilem3 8505  pigt2lt4 8507  sincosq1sgn 8534  sincosq2sgn 8535  sincosq3sgn 8536  sincosq4sgn 8537  sinq12gt0t 8538  sincosq1eq 8539  sincos6thpi 8541  cosh111lem1 8542  efgh 8546  efifolem1 8550  efifolem2 8551  efifolem3 8552  efifolem4 8553  efifolem5 8554  efifolem6 8555  efifolem7 8556  efif1lem1 8558  efif1lem3 8560  efif1lem4 8561  circgrpOLD 8571  eff1i 8578  relogeftb 8600  relogoprlem 8604  relogexpt 8609  logoprlemOLD 8622  logexptOLD 8625  elghomlem1 8649  cayleylem2 8677  uninqs 8701  elo 8704  cdrci 8738  homeofval 8754  fgsb 8794  fgsb2 8799  dtt2 8812  dmse1 8817  trran 8830  cnvtr 8832  1ded 8865  1cat 8886  ismonc 8934  hvsub4t 9055  his7t 9105  his2sub2t 9108  hial2eq2t 9122  normpyct 9162  hhph 9194  bcs2t 9198  hcau2 9205  ocorth 9294  chocuni 9302  projlem2 9317  projlem26 9341  projlem28 9343  projlem31 9346  pjtheu2 9379  pjpj0 9384  shsel3t 9408  shscl 9410  chsupss 9439  shjvalt 9450  chjvalt 9451  shjclt 9457  chjclt 9458  shsvs 9465  shslej 9467  chslejt 9550  chjcomt 9558  chub1t 9559  chdmj1t 9581  spanunsn 9633  spanpr 9634  fh1t 9692  fh2t 9693  cm2jt 9694  osumlem2 9710  osumlem3 9711  spansncv 9728  5oalem1 9730  5oalem3 9732  5oalem5 9734  3oalem2 9739  pjv 9781  pjds3 9789  hoaddclt 9815  hoeqt 9817  hoadddit 9860  hoadddirt 9861  hosubdit 9865  hosub4t 9870  hoeq1t 9887  hoeq2t 9888  counopt 9975  adjeqt 9989  brafnmult 10005  lnopsub 10028  hmopst 10074  hmopmt 10075  hmopdt 10076  hmopcot 10077  nmcopexlem1 10080  nmcopexlem3 10082  nmcopexlem5 10084  nmcopexlem6 10085  lnopcon 10092  lnfnsub 10104  nmcfnexlem1 10109  nmcfnexlem3 10111  nmcfnexlem5 10113  nmcfnexlem6 10114  lnfncon 10119  nlelsh 10122  riesz3 10124  riesz1t 10127  cnlnadjlem2 10130  cnlnadjlem6 10134  cnlnssadj 10142  adjlnopt 10148  adjmult 10153  adjaddt 10154  nmopco 10156  cnvbramult 10174  kbass2t 10176  kbass4t 10178  kbass6t 10180  leopaddt 10191  leopmul2it 10194  leoptrit 10195  leopnmidt 10196  hmopidmch 10204  cvcon3t 10335  dmdmdt 10351  mddmdt 10352  ssdmd1 10362  ssdmd2 10363  cvdmdt 10386  superpos 10403  chrelat 10413  atcv0eq 10428  atoml 10431  atcvatlem 10434  atcvat 10435  atcvat2 10436  irredlem4 10442  atcvat3 10445  atcvat4 10446  mdsymlem2 10453  mdsymlem3 10454  mdsymlem5 10456  mdsymlem8 10459  dmdsymt 10462  cdjreu 10478  cdj1 10479  cdj3lem2b 10483  cdj3lem3 10484  cdj3lem3b 10486  cdj3 10487

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