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 221

This theorem is referenced by:  ax11indalem 1407  sbccomg 2039  csbcomg 2068  csbnestg 2088  ssconb 2222  ineqan12d 2271  ifpr 2485  breqan12d 2705  copsex2g 2869  tz7.7 3001  ordin 3005  onin 3006  ontri1 3009  onelpss 3015  onsseleq 3016  ontr2 3021  unexg 3097  ordon 3141  peano4 3240  findsg 3245  vtoclr 3294  opthprc 3306  ssxp 3345  relop 3365  sotri 3535  unixp 3622  coexg 3629  funsn 3648  funco 3655  funssres 3657  fnco 3701  fco 3743  fodmrnu 3788  resdif 3816  eqfnfv 3909  eqfnfv2 3911  fconst2g 3959  isofrlem 4015  opreqan12d 4037  oprabval5 4089  curry1 4193  curry2 4196  onfununi 4209  tfrlem5 4216  tfrlem11 4222  tz7.48lem 4256  oacan 4318  oawordri 4320  oaass 4331  omord2 4334  omcan 4336  oeord 4351  oecan 4352  oeordsuc 4357  nnasuc 4365  nnmsuc 4366  nnecl 4371  nnacom 4373  nnaordi 4374  nnaword1 4384  nnmordi 4386  oaabslem 4391  oaabs 4392  omsmo 4397  brecop 4447  ecopoprtrn 4452  th3qlem1 4455  ecoprdi 4462  mapvalg 4471  pmvalg 4472  mapsn 4486  en2sn 4572  sbthlem7 4598  sbth 4602  sdomnsym 4607  xpen 4635  mapenlem1 4636  mapenlem2 4637  mapdom1 4639  mapdom2 4641  limenpsi 4652  phplem4 4658  php 4660  php3 4662  nndomo 4667  ominf 4675  pssnn 4681  unblem2 4687  isfinite2 4692  unfilem1 4694  unfilem2 4695  unfi2 4698  unifi2 4702  fodomfi 4709  inf3lem6 4763  rankxplim 4858  aceq5lem4 4884  kmlem6 4916  zorn2lem6 4939  fodom 4944  brdom6disj 4951  cardnn 4970  carddomi 4984  unxpdomlem 4993  unxpdom2 4995  ondomcard 5007  cdaval 5069  cdafi 5088  nnaun 5091  axrepndlem2 5099  axrepnd 5100  ltsopi 5170  mulclpi 5175  addcompi 5176  mulcompi 5178  distrpi 5180  ltexpi 5183  ltapi 5184  ltmpi 5185  addcmpblnq 5206  mulpipq 5209  addclpq 5212  addasspq 5217  distrpq 5221  ltsopq 5229  ltrpq 5239  genpnnp 5262  mulclprlem 5275  distrlem1pr 5281  distrlem5pr 5285  addcanpr 5306  reclem3pr 5312  mulcmpblnr 5337  addsrpr 5338  mulclsr 5347  mulasssr 5353  distrsr 5354  ltsosr 5357  1idsr 5361  00sr 5362  recexsrlem 5366  mulgt0sr 5368  suppsr3 5378  addcnsr 5407  axmulopr 5420  axmulass 5432  axdistr 5433  ax0id 5435  axcnre 5440  cnegexlem3 5501  cnegex 5502  muladd 5575  resubcl 5592  addsub4 5627  mulsub 5631  ltxrlt 5654  axltadd 5659  lenlt 5664  ltadd2 5778  leadd2 5780  ltsubadd2 5782  lesubadd2 5784  ltaddsub2 5786  leaddsub2 5788  leltadd 5800  addgtge0 5803  ltaddpos2 5806  posdif 5808  addge02 5827  subge0 5828  suble0 5829  mullt0 5835  recextlem1 5838  recextlem2 5839  recex 5840  divmuldiv 5919  conjmul 5937  prodgt02 5967  prodge02 5969  lemul2 5975  lemul2OLD 5976  lemul1a 5981  lemul1aOLD 5982  lemul2a 5983  lemul2aOLD 5984  ltmulgt12 5991  ltmuldiv2 6009  ltmuldiv2OLD 6010  ltdivmulOLD 6012  ledivmulOLD 6014  ltdivmul2 6015  lt2mul2div 6016  lt2mul2divOLD 6017  ledivmul2 6018  ledivmul2OLD 6019  lemuldiv2 6021  lemuldiv2OLD 6022  lereci 6025  ledivdiv 6035  lediv2 6036  ltdiv23 6037  lediv23 6038  max1 6060  max2 6062  min1 6064  min2 6065  nnaddcl 6085  nnmulcl 6086  nnleltp1 6100  nnltp1le 6101  nnaddm1cl 6104  nndiv 6105  rpaddcl 6206  rpmulcl 6207  rpdivcl 6208  reuuninegi 6234  nnrecl 6240  supxrbnd1 6263  supxrbnd2 6264  nn0nnaddcl 6294  nn0leltp1 6296  nn0ltlem1 6297  nn0sub 6329  zaddcl 6333  zsubcl 6336  znnsub 6345  znn0sub 6346  zmulcl 6348  zleltp1 6350  nn0lem1lt 6353  nnlem1lt 6354  nnltlem1 6355  zdiv 6356  z2ge 6359  zextle 6360  zextlt 6361  btwnnz 6363  prime 6366  zneo 6371  peano2uz2 6372  uzind 6376  uzindOLD 6379  uzwo4OLD 6381  zmax 6392  rebtwnz 6394  qre 6398  qaddcl 6408  qnegcl 6409  qsubcl 6411  irradd 6416  qbtwnre 6418  qbtwnxr 6419  flge 6431  fllt 6432  flval3 6438  fladdz 6443  flzadd 6444  quoremnn0ALT 6452  quoremnn0 6453  fldiv 6456  modlt 6463  flmulnn0 6467  flmulnn0OLD 6468  modmulnn 6469  zmodcl 6470  modcyc 6475  monoord 6482  elioc2 6516  elico2 6517  elicc2 6518  icoshftf1oii 6536  snunioolem 6541  ioojoin 6543  uzneg 6556  uz11 6559  eluzp1m1 6560  eluzp1p1 6562  uzaddcl 6576  uzwo 6582  uzwoOLD 6583  indstr 6588  elfz1eq 6620  fzn 6621  elfz2nn0 6625  fznn0sub2 6629  fzaddel 6630  fzsubel 6631  fzopth 6632  fzsuc 6636  fzrev2 6643  fzrev3 6645  fzrevral 6650  fzrevral3 6652  fzshftral 6653  fseqsupcl 6656  om2uzlti 6661  om2uzlt2i 6662  om2uzf1oi 6664  ser1add2i 6703  ser1addi 6704  seqzp1 6743  seqzval2 6748  seqzrn2 6751  expp1 6769  expcllem 6770  expadd 6791  expmul 6792  expsub 6793  expsubOLD 6794  expordi 6797  expcan 6798  expord 6799  expwordi 6800  expmwordi 6803  lt2sq 6827  le2sq 6828  bernneq 6849  bernneqOLD 6850  bernneq2 6851  expnbnd 6852  digit2 6855  digit1 6856  nn0opthlem2 6866  sqrlem6 6879  sqrlem12 6885  sqrlei 6908  sqrlti 6909  sqr4 6918  sqr9 6919  sqr2irr 6930  crre 6970  crim 6971  mulre 6978  resub 7007  imsub 7010  cjsub 7017  cjreim 7029  cjreim2 7030  cj11OLD 7032  absreimsq 7058  absreim 7059  sqabs 7071  absdiflt 7086  absdifle 7087  abssuble0 7099  absmax 7100  abs2difabs 7106  seq1bndi 7113  cau2i 7116  cau4ii 7121  cau5i 7122  cvg1i 7123  cvg1 7124  cvg3i 7126  caubndi 7129  caurei 7130  cauimi 7131  ser1absdiflem 7132  ser1absdifi 7133  facdiv 7145  facwordi 7147  faclbnd 7148  faclbnd3 7150  faclbnd4lem4 7154  faclbnd5 7156  faclbnd6 7157  facavg 7158  bcval4 7164  bccmpl 7165  bccl2 7174  fsum1ps 7221  fsumsplit 7223  fsumadd 7225  fsumrev 7232  fsumrev2 7233  fsumshft 7234  fsumshftm 7235  fsumcmp 7243  fsumcmpndx2 7245  fsumabs 7246  fsumabs2mul 7247  binomlem1 7269  binomlem2 7270  binomlem4 7272  binomlem5 7273  clm3i 7282  climshfti 7307  climge0 7315  climaddlem3 7319  climmullem1 7323  climmullem4 7326  climmullem5 7327  climmullem8 7330  climsub 7333  clim2serz 7337  clim2serzi 7348  climserzlei 7350  climcaui 7359  caucvglem5 7364  caucvglem6 7365  caucvgi 7366  serzf0i 7372  ser1cmp2lem 7379  ser1cmp2i 7380  cvgcmp3ci 7390  reccnv 7422  infcvglem1 7425  geoseri 7439  cvgratlem2ALT 7453  cvgratlem1 7455  cvgratlem2 7456  fsum0diaglem2 7462  fsum0diag4 7466  negfcncfi 7474  mulc1cncf 7484  ivthlem6 7491  ivthlem7 7492  ivthlem8 7493  efseq0ex 7516  efaddlem3 7545  efaddlem5 7547  efaddlem6 7548  efaddlem11 7553  efaddlem13 7555  efaddlem14 7556  efaddlem17 7559  efaddlem19 7561  abspef01tlubi 7603  reeff1o 7634  efieq 7658  sinsub 7663  cossub 7664  subsin 7666  addcos 7667  subcos 7668  nn0ennn 7709  xpnnen 7711  znnenlem 7713  znnen 7714  infpnlem1 7718  infpn2 7721  infxpidmlem1 7764  infxpidmlem11 7774  infxpidmlem12 7775  infunabs 7777  infcdaabs 7778  infdif 7780  infxpabs 7782  infmap1 7785  infpss 7786  iunctb 7787  unctb 7789  alephmul 7795  subbas 7856  subtop 7858  retopbas 7865  neiint 7929  innei 7946  islp2 7957  iscn 7968  iscnp 7970  cnco 7978  cnconst 7990  sncld 7997  metxplem1 8036  metxplem2 8037  metxp 8044  bl2in 8053  opnin 8079  metcnp 8098  metcn 8100  cncfmet 8116  remetdval 8119  bl2ioo 8122  ioo2bl 8123  blssioo 8124  tgioolem 8125  lmuni 8162  caussi 8165  causs 8166  lmle 8171  xplm 8186  xpcn 8187  bcthlem8 8217  bcthlem9 8218  bcthlem18 8227  bcthlem20 8229  bcthlem21 8230  gxnn0suc 8320  gxnn0add 8330  gxadd 8331  gxsub 8332  gxnn0mul 8333  gxmul 8334  gxmodid 8335  abldivdiv4 8350  ablmul 8372  ghgrpilem1 8374  ghsubgi 8379  vcoprnelem 8444  vacnlem3 8584  sqcn 8589  nmcnilem 8591  sm1cnilem 8601  nvo00 8678  nmoge0 8684  nmorepnf 8685  nmolb 8688  nmoub3i 8690  blocnilem 8719  blocni 8720  cnph 8734  ipasslem1 8746  ipasslem2 8747  ipasslem4 8749  ipasslem8 8753  ipasslem11 8756  ipblnfi 8772  phoeqi 8774  ajval 8778  ubthlem7 8793  ubthlem8 8794  ubthlem9 8795  ubthlem10 8796  ubthlem11 8797  ubthlem12 8798  ubthlem12OLD 8799  ubthlem13 8800  ubthlem13OLD 8801  ubthlem14 8802  minveclem9 8813  minveclem16 8820  minveclem18 8822  minveclem19 8823  minveclem21 8825  minveclem24 8828  minveclem25 8829  minveclem26 8830  minveclem27 8831  minveclem28 8832  minveclem30 8834  minveclem31 8835  minveclem36 8840  minveclem38 8842  minveceu 8843  htthlem6 8887  htthlem8 8889  pilem2 8939  pilem3 8940  pigt2lt4 8942  sincosq1sgn 8971  sincosq2sgn 8972  sincosq3sgn 8973  sincosq4sgn 8974  sinq12gt0t 8975  sincosq1eq 8977  sincos6thpi 8979  cosh111lem1 8986  efgh 8990  efifolem1 8994  efifolem2 8995  efifolem3 8996  efifolem4 8997  efifolem5 8998  efifolem6 8999  efifolem7 9000  efif1lem1 9002  efif1lem3 9004  efif1lem4 9005  eff1i 9016  relogeftb 9037  relogoprlem 9041  relogexp 9046  hvsub4 9181  his7 9232  his2sub2 9235  hial2eq2 9249  normpyc 9289  hhph 9321  bcs2 9325  hcau2 9331  hhssabli 9408  hhssnv 9410  hhsscms 9426  ocorth 9440  chocunii 9448  projlem2 9463  projlem26 9487  projlem28 9489  projlem31 9492  pjtheu2i 9526  pjpj0i 9531  shsel3 9555  shscli 9557  chsupss 9586  shjval 9597  chjval 9598  shjcl 9604  chjcl 9605  shsvsi 9612  shsleji 9614  chslej 9697  chjcom 9705  chub1 9706  chdmj1 9728  spanunsni 9778  spanpr 9779  fh1 9837  fh2 9838  cm2j 9839  osumlem2 9857  osumlem3 9858  spansncvi 9875  5oalem1 9877  5oalem3 9879  5oalem5 9881  3oalem2 9886  pjvi 9928  pjds3i 9936  hoaddcl 9964  hoeq 9966  hoadddi 10009  hoadddir 10010  hosubdi 10014  hosub4 10019  hoeq1 10036  hoeq2 10037  counop 10125  adjeq 10139  brafnmul 10155  lnopsubi 10177  hmops 10224  hmopm 10225  hmopd 10226  hmopco 10227  nmcopexlem1 10230  nmcopexlem3 10232  nmcopexlem5 10234  nmcopexlem6 10235  lnopconi 10242  lnfnsubi 10254  nmcfnexlem1 10259  nmcfnexlem3 10261  nmcfnexlem5 10263  nmcfnexlem6 10264  lnfnconi 10269  nlelshi 10272  riesz3i 10274  riesz1 10277  cnlnadjlem2 10280  cnlnadjlem6 10284  cnlnssadj 10292  adjlnop 10298  adjmul 10304  adjadd 10305  nmopcoi 10307  cnvbramul 10328  kbass2 10330  kbass4 10332  kbass6 10334  leopadd 10345  leopmul2i 10348  leoptri 10349  leopnmid 10351  hmopidmchi 10359  cvcon3 10492  dmdmd 10508  mddmd 10509  ssdmd1 10521  ssdmd2 10522  cvdmd 10545  superpos 10562  chrelati 10572  atcv0eq 10588  atomli 10591  atcvatlem 10594  atcvati 10595  atcvat2i 10596  irredlem4 10602  atcvat3i 10605  atcvat4i 10606  mdsymlem2 10613  mdsymlem3 10614  mdsymlem5 10616  mdsymlem8 10619  dmdsym 10622  cdjreui 10641  cdj1i 10642  cdj3lem2b 10646  cdj3lem3 10647  cdj3lem3b 10649  cdj3i 10650  elghomlem1 10667  cayleylem2 10695  uninqs 10730  elo 10733  unpde2eg2 10825  setwoe 10828  cdrci 10994  osneisi 11018  homeofval 11022  fgsb 11082  fgsb2 11086  limfillem2 11102  dtt2 11110  altretop 11144  dmse1 11146  trran 11159  cnvtr 11161  1ded 11192  1cat 11213  ismonc 11269  idsubfun 11312  dmsdtriord 11408  fictb 11423  omsubsuc2 11439  omsubsdom 11442  omsubdom 11443  omsubel 11444  omsubss 11445  opncldf1 11454  opnregcld 11467  cldregopn 11468  subsubtop 11479  subcld 11480  uncomp 11490  connsub 11502  reconn 11512  ivthALT 11515  filmapss 11696  flimff 11707  fclusff 11735  istail 11757  gacan 11782  upxp 11822  indexa 11845  fzm1 11867  sdclem2 11876  sdc 11877  incsequz 11879  incsequz2 11880  fsumlt 11884  csbrni 11895  incld 11899  mettrifi2 11913  geomcau 11914  iccshftr 11922  iccshftl 11924  iccdil 11926  icccntr 11928  lincmb01cmp 11942  lincmb01icc 11943  ishomeo2 11957  haustlmu 11967  lmtlm 11969  txuni 11975  tx1cn 11976  tx2cn 11977  uptx 11978  txcnopab 11980  txsubsp 11983  sstotbnd 11992  totbndbnd 12000  ismtyval 12003  isismty 12004  ismtyhmeo 12007  ismtyres 12010  heiborlem12 12022  heiborlem15 12025  heiborlem16 12026  heiborlem26 12036  heiborlem28 12038  heiborlem32 12042  heiborlem33 12043  heiborlem35 12045  heiborlem38 12048  bfplem8 12061  recms 12066  rrnmet 12072  rrndstprj2 12074  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  iccbnd 12082  phtpycom 12092  phtpycolem2 12094

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 145  df-an 223

Copyright terms: Public domain