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 1361  sbccomg 1979  csbcomg 2007  csbnestg 2026  ssconb 2160  ineqan12d 2209  ifpr 2417  breqan12d 2622  copsex2g 2783  unexg 2865  tz7.7 2963  ordin 2967  onin 2968  ontri1 2971  ordon 2977  onelpsst 2988  onsseleq 2989  ontr2 2994  peano4 3142  findsg 3147  vtoclr 3201  opthprc 3211  ssxp 3246  relop 3265  sotri 3429  unixp 3503  coexg 3510  funsn 3529  funco 3536  funssres 3538  fnco 3581  fco 3621  fodmrnu 3665  eqfnfv 3782  fconst2g 3830  isofrlem 3886  tfrlem5 3900  tfrlem11 3906  tz7.48lem 3940  opreqan12d 3964  oprabval5 4014  curry1 4082  oacan 4166  oawordri 4168  oaass 4179  omord2 4182  omcan 4184  oeord 4199  oecan 4200  oeordsuc 4205  nnasuc 4209  nnmsuc 4210  nnecl 4215  nnacom 4217  nnaordi 4218  nnaword1 4228  nnmordi 4230  oaabslem 4235  oaabs 4236  omsmo 4241  brecop 4290  ecopoprtrn 4295  th3qlem1 4298  ecoprdi 4305  mapvalg 4314  pmvalg 4315  mapsn 4329  en2sn 4412  sbthlem7 4433  sbth 4437  sdomnsym 4442  xpen 4468  mapenlem1 4469  mapenlem2 4470  mapdom1 4472  mapdom2 4474  limenpsi 4485  phplem4 4491  php 4493  php3 4495  nndomo 4500  ominf 4508  pssnn 4513  unblem2 4518  isfinite2 4523  unfilem1 4524  unfilem2 4525  unfi2 4529  unifi2 4533  fodomfi 4540  inf3lem6 4590  rankxplim 4684  aceq5lem4 4710  kmlem6 4742  zorn2lem6 4765  fodom 4770  brdom6disj 4777  cardnn 4796  carddomi 4807  unxpdomlem 4815  unxpdom2 4817  ondomcard 4829  cdavalt 4891  cdafi 4908  axrepndlem2 4917  axrepnd 4918  ltsopi 4988  mulclpi 4993  addcompi 4994  mulcompi 4996  distrpi 4998  ltexpi 5001  ltapi 5002  ltmpi 5003  addcmpblnq 5024  mulpipq 5027  addclpq 5030  addasspq 5035  distrpq 5039  ltsopq 5047  ltrpq 5057  genpnnp 5080  mulclprlem 5093  distrlem1pr 5099  distrlem5pr 5103  addcanpr 5124  reclem3pr 5130  mulcmpblnr 5155  addsrpr 5156  mulclsr 5165  mulasssr 5171  distrsr 5172  ltsosr 5175  1idsr 5179  00sr 5180  recexsrlem 5184  mulgt0sr 5186  suppsr3 5196  addcnsr 5225  axmulopr 5238  axmulass 5250  axdistr 5251  ax0id 5253  axcnre 5258  cnegextlem3 5319  cnegext 5320  muladdt 5393  resubclt 5410  addsub4t 5445  mulsubt 5449  ltxrltt 5472  axltadd 5477  lenltt 5482  ltadd2t 5598  leadd2t 5600  ltsubadd2t 5602  lesubadd2t 5604  ltaddsub2t 5606  leaddsub2t 5608  addgtge0t 5622  ltaddpos2t 5625  posdift 5627  addge02t 5646  subge0t 5647  suble0t 5648  recextlem1 5655  recextlem2 5656  recext 5657  divmuldivt 5736  divdivdivt 5741  conjmult 5753  prodgt02t 5783  prodge02t 5785  lemul2t 5789  lemul1it 5793  lemul1itOLD 5794  lemul2it 5795  lemul2itOLD 5796  ltmulgt12t 5803  ltmuldiv2t 5818  ltdivmult 5819  ledivmult 5820  ltdivmul2t 5821  lt2mul2divt 5822  ledivmul2t 5823  lemuldiv2t 5825  lerec 5828  ledivdivt 5838  lediv2t 5839  max1 5863  max2 5865  min1 5867  min2 5868  nnaddclt 5888  nnmulclt 5889  nnleltp1t 5901  nnltp1let 5902  nnaddm1clt 5905  nndivt 5906  reuunineg 6013  nnreclt 6019  supxrbnd1 6042  supxrbnd2 6043  nn0nnaddclt 6073  nn0leltp1t 6075  nn0ltlem1t 6076  nn0subt 6108  zaddclt 6112  zsubclt 6115  znnsubt 6124  znn0subt 6125  zmulclt 6127  zleltp1t 6129  nn0lem1ltt 6132  nnlem1ltt 6133  nnltlem1t 6134  z2get 6135  zextlet 6136  zextltt 6137  btwnnzt 6139  primet 6142  zneo 6147  zneoOLD 6148  peano2uz2 6149  uzind 6153  uzindOLD 6156  uzwo4OLD 6158  zmax 6168  rebtwnz 6170  flget 6178  flltt 6179  flval3t 6182  fladdzt 6187  qret 6197  qnegclt 6208  qsubclt 6210  qrecclt 6211  qbtwnre 6216  qbtwnxr 6217  rpaddclt 6227  rpmulclt 6228  rpdivclt 6229  monoord 6231  om2uzlt 6235  om2uzlt2 6236  om2uzf1o 6238  ser1add2 6275  ser1add 6276  elioc2t 6322  elico2t 6323  elicc2t 6324  ioonegt 6339  icoshftf1oi 6342  snunioolem 6347  uznegit 6361  uz11t 6364  eluzp1m1t 6365  eluzp1p1t 6367  uzaddclt 6381  uzwo 6387  uzwoOLD 6388  indstr 6393  elfz1eqt 6424  fznt 6425  elfz2nn0t 6427  fznn0sub2t 6431  fzaddelt 6432  fzsubelt 6433  fzoptht 6434  fzrev2t 6444  fzrev3t 6446  fzrevralt 6451  fzrevral3t 6453  fzshftralt 6454  fseqsupcl 6457  seqzp1 6480  seqzval2t 6485  seqzrn2 6488  expp1t 6506  expcllem 6507  expaddt 6527  expmult 6528  expsubt 6529  expordit 6531  expcant 6532  expordt 6533  expwordit 6534  expmwordit 6537  lt2sqt 6561  le2sqt 6562  bernneq 6583  bernneq2 6584  expnbndt 6585  nn0opthlem2 6595  sqrlem6 6608  sqrlem12 6614  sqrle 6637  sqrlt 6638  sqr4 6647  sqr9 6648  sqr2irr 6659  crret 6702  crretOLD 6703  crimt 6704  crimtOLD 6705  resubt 6741  imsubt 6744  cjsubt 6751  cjreimt 6763  cjreim2t 6764  cj11t 6765  absreimsqt 6791  absreimt 6792  absdifltt 6821  absdiflet 6822  abssuble0t 6834  abs2difabst 6840  seq1bnd 6847  cau2 6850  cau4i 6855  cau5 6856  cvg1i 6857  cvg1 6858  cvg3 6860  caubnd 6863  caure 6864  cauim 6865  ser1absdiflem 6866  ser1absdif 6867  facdivt 6879  facwordit 6881  faclbnd 6882  faclbnd3 6884  faclbnd4lem4 6888  faclbnd5 6890  faclbnd6 6891  facavgt 6892  bcval4t 6899  bccmplt 6900  bccl2t 6909  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  fsumrev 6967  fsumrev2 6968  fsumshft 6969  fsumshftm 6970  fsumcmp 6978  fsumcmpndx2 6980  fsumabs 6981  fsumabs2mul 6982  binomlem1 7004  binomlem2 7005  binomlem4 7007  binomlem5 7008  clm3 7017  climshft 7041  climge0 7049  climaddlem3 7052  climmullem1 7056  climmullem5 7060  climmullem8 7063  climsub 7066  clim2serzt 7070  clim2serz 7081  climserzle 7083  climcau 7092  caucvglem5 7097  caucvglem6 7098  caucvg 7099  serzf0 7105  ser1f0 7106  ser1cmp2lem 7112  ser1cmp2 7113  cvgcmp3c 7122  reccnv 7153  infcvglem1 7156  geoser 7169  cvgratlem2ALT 7183  cvgratlem1 7185  cvgratlem2 7186  fsum0diaglem2 7192  fsum0diag4 7196  negfcncf 7204  mulc1cncf 7214  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  ivthlem6OLD 7230  ivthlem7OLD 7231  efseq0ex 7253  efaddlem3 7282  efaddlem5 7284  efaddlem6 7285  efaddlem11 7290  efaddlem13 7292  efaddlem14 7293  efaddlem17 7296  efaddlem19 7298  abspef01tlub 7336  reeff1o 7368  efieq 7392  sinsubt 7397  cossubt 7398  subsint 7400  addcost 7401  subcost 7402  nn0ennn 7439  xpnnen 7441  znnenlem 7443  znnenlemOLD 7444  znnen 7445  infpnlem1 7449  infpn2 7452  infxpidmlem1 7495  infxpidmlem11 7505  infxpidmlem12 7506  infunabs 7508  infcdaabs 7509  infdif 7511  infxpabs 7513  infmap1 7516  iunctb 7517  unctb 7519  alephmul 7525  subbas 7586  subtop 7588  retopbas 7597  neiint 7660  innei 7677  islp2 7688  iscn 7698  iscnp 7700  cnco 7707  cnconst 7719  sncld 7726  metxplem1 7766  metxplem2 7767  metxp 7774  bl2in 7783  opnin 7809  metcnp 7826  metcn 7828  cncfmet 7844  remetdval 7847  bl2ioo 7850  ioo2bl 7851  blssioo 7852  tgioolem 7853  lmuni 7886  caussi 7889  causs 7890  lmle 7895  xplm 7909  xpcn 7910  bcthlem8 7940  bcthlem9 7941  bcthlem18 7950  bcthlem20 7952  bcthlem21 7953  resgrprnOLD 8031  abldivdiv4 8046  ablmul 8068  ghgrpilem1 8070  ghsubgi 8075  vcoprnelem 8135  sqcn 8270  nmcnilem 8272  sm1cnilem 8281  nvo00 8356  nmoge0 8362  nmorepnf 8363  nmolb 8366  nmoub3i 8368  blocnilem 8395  blocni 8396  cnph 8409  ipasslem1 8421  ipasslem2 8422  ipasslem4 8424  ipasslem8 8428  ipasslem11 8431  ipblnfi 8447  phoeqi 8449  ubthlem7 8466  ubthlem8 8467  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  ubthlem12 8471  ubthlem13 8472  ubthlem14 8473  minveclem9 8484  minveclem16 8491  minveclem18 8493  minveclem19 8494  minveclem21 8496  minveclem24 8499  minveclem25 8500  minveclem26 8501  minveclem27 8502  minveclem28 8503  minveclem30 8505  minveclem31 8506  minveclem36 8511  minveclem38 8513  minveceu 8514  htthlem6 8555  htthlem8 8557  pilem2 8591  pilem3 8592  pigt2lt4 8594  sincosq1sgn 8621  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  sinq12gt0t 8625  sincosq1eq 8626  sincos6thpi 8628  cosh111lem1 8629  efgh 8633  efifolem1 8637  efifolem2 8638  efifolem3 8639  efifolem4 8640  efifolem5 8641  efifolem6 8642  efifolem7 8643  efif1lem1 8645  efif1lem3 8647  efif1lem4 8648  circgrpOLD 8658  eff1i 8665  relogeftb 8687  relogoprlem 8691  relogexpt 8696  logoprlemOLD 8709  logexptOLD 8712  hvsub4t 8827  his7t 8877  his2sub2t 8880  hial2eq2t 8894  normpyct 8934  hhph 8966  bcs2t 8970  hcau2 8976  hhssabl 9053  hhssnv 9054  hhsscms 9067  ocorth 9080  chocuni 9088  projlem2 9103  projlem26 9127  projlem28 9129  projlem31 9132  pjtheu2 9165  pjpj0 9170  shsel3t 9194  shscl 9196  chsupss 9225  shjvalt 9236  chjvalt 9237  shjclt 9243  chjclt 9244  shsvs 9251  shslej 9253  chslejt 9336  chjcomt 9344  chub1t 9345  chdmj1t 9367  spanunsn 9419  spanpr 9420  fh1t 9478  fh2t 9479  cm2jt 9480  osumlem2 9496  osumlem3 9497  spansncv 9514  5oalem1 9516  5oalem3 9518  5oalem5 9520  3oalem2 9525  pjv 9567  pjds3 9575  hoaddclt 9601  hoeqt 9603  hoadddit 9646  hoadddirt 9647  hosubdit 9651  hosub4t 9656  hoeq1t 9673  hoeq2t 9674  counopt 9761  adjeqt 9775  brafnmult 9791  lnopsub 9814  hmopst 9860  hmopmt 9861  hmopdt 9862  hmopcot 9863  nmcopexlem1 9866  nmcopexlem3 9868  nmcopexlem5 9870  nmcopexlem6 9871  lnopcon 9878  lnfnsub 9890  nmcfnexlem1 9895  nmcfnexlem3 9897  nmcfnexlem5 9899  nmcfnexlem6 9900  lnfncon 9905  nlelsh 9908  riesz3 9910  riesz1t 9913  cnlnadjlem2 9916  cnlnadjlem6 9920  cnlnssadj 9928  adjlnopt 9934  adjmult 9939  adjaddt 9940  nmopco 9942  cnvbramult 9960  kbass2t 9962  kbass4t 9964  kbass6t 9966  leopaddt 9977  leopmul2it 9980  leoptrit 9981  leopnmidt 9982  hmopidmch 9990  cvcon3t 10121  dmdmdt 10137  mddmdt 10138  ssdmd1 10148  ssdmd2 10149  cvdmdt 10172  superpos 10189  chrelat 10199  atcv0eq 10214  atoml 10217  atcvatlem 10220  atcvat 10221  atcvat2 10222  irredlem4 10228  atcvat3 10231  atcvat4 10232  mdsymlem2 10239  mdsymlem3 10240  mdsymlem5 10242  mdsymlem8 10245  dmdsymt 10248  cdjreu 10264  cdj1 10265  cdj3lem2b 10269  cdj3lem3 10270  cdj3lem3b 10272  cdj3 10273  elghomlem1 10287  cayleylem2 10317  uninqs 10342  elo 10345  cdrci 10381  homeofval 10403  fgsb 10444  fgsb2 10449  dtt2 10462  dmse1 10467  trran 10480  cnvtr 10482  1ded 10515  1cat 10536  ismonc 10584

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