Theorem sylan2 451

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
sylan2.2	|- (th -> ps)

Assertion

Ref	Expression
sylan2	|- ((ph /\ th) -> ch)

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 373	. . 3 |- (ph -> (ps -> ch))
3		sylan2.2	. . 3 |- (th -> ps)
4	2, 3	syl5 21	. 2 |- (ph -> (th -> ch))
5	4	imp 350	1 |- ((ph /\ th) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sylan2b 452  sylan2br 453  syl2an 454  sylanr1 462  sylanr2 463  ax11indalem 1361  ax11inda2ALT 1362  elabgt 1886  sbciegft 1949  hbsbc1gd 1973  hbsbcgd 1974  hbcsb1gd 2017  hbcsbgd 2018  csbnestg 2026  sbcnestg 2028  sspr 2466  ssiun 2582  opth1gOLD 2788  uniexb 2897  trssord 2955  ordelssne 2964  onint 2996  onint0 2997  onnmin 3005  onsssuc 3048  onsucmin 3062  ordsucun 3072  nlimsucg 3102  ordunisuc2 3105  peano5 3143  findsg 3147  tfindsg 3152  tfindsg2 3153  cnvexg 3505  coexg 3510  funimass2 3559  cofunexg 3566  cofunex2g 3567  dmfex 3640  funbrfv 3735  eqfnfv 3782  fvimacnvi 3789  fvimacnvALT 3794  funiunfv 3851  isofrlem 3886  tfrlem8 3903  tfrlem9 3904  tfrlem11 3906  tfr3 3911  foprrn 4020  fnoprvalrn 4023  oasuc 4147  omsuc 4149  oalim 4151  omlim 4152  oalimcl 4178  oaass 4179  omlimcl 4193  odi 4194  omass 4195  oneo 4196  oelim2 4206  nnaordex 4233  nnawordex 4234  oaabslem 4235  ecoprass 4304  ecoprdi 4305  mapex 4312  f1oen2g 4375  f1oeng 4376  domentr 4402  undom 4418  pwuninelg 4467  mapunen 4482  ssenen 4484  phplem3 4490  phplem4 4491  php 4493  php3 4495  onomeneq 4498  omsucdom 4502  ssfi 4515  unbnn2 4522  unfi 4528  unifi 4532  fodomfi 4540  iunfi 4543  pm54.43 4546  omex 4599  aceq3 4705  aceq5 4712  aceq6b 4714  ac5b 4725  zorn2lem3 4762  imadomg 4778  sucdom 4814  ondomon 4828  alephnbtwn 4840  alephordi 4846  alephval2 4874  cfom 4888  axrepndlem2 4917  axpowndlem4 4924  axinfndlem1 4929  axacndlem5 4935  addclpi 4992  addasspi 4995  mulasspi 4997  distrpi 4998  mulcanpi 4999  indpi 5006  ltapq 5048  ltrpq 5057  prcdpq 5069  genpass 5084  distrlem1pr 5099  distrlem2pr 5100  distrlem4pr 5102  psslinpr 5107  prlem934b 5110  ltexprlem6 5119  ltexprlem7 5120  prlem936b 5126  prlem936 5127  reclem3pr 5130  reclem4pr 5131  recexsrlem 5184  suppsr3 5196  pre-axsup 5263  cnegextlem1 5317  cnegextlem3 5319  cnegext 5320  subnegt 5366  subdit 5399  1re 5407  resubclt 5410  mulneg2t 5424  negsubdit 5429  submul2t 5432  subsub2t 5433  nnncan1t 5439  addsub4t 5445  xrret 5542  le2tri3 5563  ltaddsubt 5605  leaddsubt 5607  lenegcon2t 5632  recextlem1 5655  recextlem2 5656  recext 5657  divnegt 5730  letrp1t 5772  lerec2t 5837  ledivdivt 5838  lediv12it 5844  ledivp1t 5853  nndivt 5906  nndivtrt 5907  lble 5994  sup2 5998  dfinfmr 6014  nnunb 6017  arch 6018  bndndx 6020  xrsupsslem 6023  xrinfmsslem 6024  supxrunb1 6036  nn0ge0t 6064  nn0addclt 6067  nn0leltp1t 6075  nn0addge1t 6077  nn0addge2t 6078  zaddclt 6112  zsubclt 6115  zrevaddclt 6117  elnn0nn 6118  zltp1let 6128  zleltp1t 6129  zltlem1t 6131  peano2uz2 6149  uzind 6153  uzindOLD 6156  uzwo4OLD 6158  uzwo3lem1 6164  zmax 6168  zbtwnre 6169  rebtwnz 6170  flget 6178  flwordit 6183  flbit 6184  fladdzt 6187  qaddclt 6207  qsubclt 6210  qrecclt 6211  qdivclt 6212  qrevaddclt 6213  qbtwnre 6216  qsqueeze 6218  seq1rn2 6258  ser1recl 6268  elioc2t 6322  elico2t 6323  elicc2t 6324  icounlem 6345  eluzp1lt 6366  uzwo 6387  uzwoOLD 6388  fzss2t 6436  fzrev2t 6444  fzrev3it 6447  fzrevralt 6451  fsequb 6455  fsequb2 6456  fseqsupub 6458  seqzp1 6480  seqzval2t 6485  seqzeq 6487  seqzrn2 6488  seqzrn 6489  ser0cl1 6496  expnnvalt 6504  expp1t 6506  expm1t 6515  expeq0t 6517  expge0t 6522  expgt1t 6523  expge1t 6524  bernneq 6583  replimt 6692  resubt 6741  imsubt 6744  cjsubt 6751  sqabsaddt 6783  sqabssubt 6784  seq1bnd 6847  cau3ir 6852  cau5i 6854  cvg2 6859  facclt 6877  facdivt 6879  faclbnd4lem3 6887  faclbnd4lem4 6888  faclbnd5 6890  bccmplt 6900  fsum1s 6947  fsump1s 6951  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  fsumcom 6966  fsumrev 6967  fsumshft 6969  fsummulc1 6971  fsummulc2 6972  fsum2mul 6975  fsumconst 6976  fsumcmp 6978  fsumcmp0 6979  fsumcmpndx2 6980  fsumabs 6981  fsumabs2mul 6982  serzcl2t 6987  serzcmp0 6993  binomlem1 7004  binomlem2 7005  binomlem5 7008  binomlem6 7009  clm4 7018  clm4le 7019  clm4f 7020  clm4at 7028  climfnn 7030  2climnn 7039  2climnn0 7040  iserzshft2 7044  climge0 7049  climaddlem3 7052  climaddc1 7054  climmullem3 7058  climmullem5 7060  climmullem8 7063  climmulc2 7065  climsubc2 7067  clim2serzt 7070  iserzmulc1 7072  iserzcmp 7078  clim2serz 7081  climserzle 7083  climsup 7091  caucvglem6 7098  isumreclt 7145  expcnv 7168  geoisum1c 7180  cvgratlem1ALT 7182  cvgratlem2ALT 7183  cvgratlem1 7185  cvgratlem2 7186  cvgratlem4 7188  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag 7193  fsum0diag2 7194  mulc1cncf 7214  ivthlem7 7222  ivthlem7OLD 7231  efcltlem1 7246  erelem1 7261  erelem3 7263  efaddlem5 7284  efaddlem6 7285  efsubt 7313  efexpt 7314  reeftlclt 7322  sinsubt 7397  cossubt 7398  demoivreALT 7427  acdc5lem1 7433  acdcALT 7438  znnenlem 7443  znnenlemOLD 7444  unbenlem 7447  ruclem13 7465  infxpidmlem1 7495  infxpidmlem8 7502  infxpidmlem11 7505  infxpidmlem12 7506  infdif 7511  iunopnt 7541  istps3 7550  eltgt 7560  eltg2t 7561  tgclt 7566  tgval3t 7567  basgen2t 7581  bastop 7584  subbas2 7587  fctop 7592  clsval2 7627  ntrss 7630  isnei 7659  isneip 7661  neips 7668  islp2 7688  iscncl 7709  metreslem 7762  blin 7792  blss 7793  isopn4 7802  opnin 7809  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metcnss 7837  metcnss2 7838  lmbr 7866  lmnn 7873  lmuni 7886  causs 7890  lmfexlem2 7892  metelcls 7900  metcnp4 7904  xplmi2 7908  opr1cn 7912  lmcau 7930  bcthlem1 7933  bcthlem9 7941  bcthlem10 7942  bcthlem14 7946  bcthlem16 7948  bcthlem21 7953  grpidinvlem1 7982  grpidinvlem2 7983  grpideu 7987  resgrprn 8030  grplactfval 8032  ablnncan 8049  issubgi 8059  ablmul 8068  ghgrpilem4 8073  isvc 8138  isnv 8170  nvmul0or 8212  imsmetlem 8261  nvlmle 8268  nmcnilem 8272  sm1cnilem 8281  ipcl 8299  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem5 8311  ip1cnilem6 8312  sspival 8331  lnocoi 8352  nmosetre 8359  nmoge0 8362  nmoub3i 8368  nmobndi 8370  nmlno0lem 8385  blo3i 8393  blometi 8394  blocnilem 8395  cnph 8409  ipasslem2 8422  ipasslem5 8425  ipdi 8434  ipsubdi 8440  ipblnfi 8447  ajmoi 8450  ubthlem3 8462  ubthlem5 8464  ubthlem6 8465  ubthlem7 8466  ubthlem10 8469  ubthlem11 8470  minveclem24 8499  minveclem25 8500  minveclem28 8503  htthlem8 8557  htthlem9 8558  sinper 8609  cosper 8610  efifolem7 8643  efif1lem5 8649  circgrpOLD 8658  efper 8669  axgroth3 8718  hvsubopr 8806  hvsubclt 8808  hvaddsubvalt 8823  hvpncant 8829  hvaddeq0t 8857  hvmulcant 8860  his5t 8874  his7t 8877  his2sub2t 8880  hlimcaui 9027  hhssnv 9054  shorth 9084  occllem6 9094  projlem25 9126  projlem26 9127  pjvalt 9154  pjeq2t 9156  chsscon2t 9340  chpsscon2t 9343  chdmm3t 9365  chdmm4t 9366  chdmj3t 9369  chdmj4t 9370  chj4t 9373  spansnmul 9403  cmcm2t 9476  fh1t 9478  fh2t 9479  cm2jt 9480  spansnsclt 9510  spansncv 9514  5oalem4 9519  homulclt 9602  homco1t 9644  homulasst 9645  hoadddit 9646  hosubnegt 9650  honegsubdit 9653  hosubsub2t 9655  hosub4t 9656  adjmo 9675  adjsymt 9676  cnvadj 9733  nmopub2tALT 9750  unoplint 9760  counopt 9761  nmfnleub2t 9766  hmoplint 9782  braaddt 9785  bramult 9786  kbmult 9795  lnopmult 9807  lnopaddmul 9813  lnopsubmul 9815  homco2t 9817  nmlnop0ALT 9835  lnopm 9840  lnophs 9841  lnopeq0 9847  unopbdt 9855  hmopdt 9862  nmophm 9876  lnopcon 9878  lnfnmul 9888  lnfnaddmul 9889  lnfncon 9905  nlelsh 9908  riesz3 9910  cnlnadjlem6 9920  adjlnopt 9934  adjmult 9939  adjco 9947  cnvbramult 9960  leopnmidt 9982  hmopidmpj 9991  pjadjco 10000  pjss1co 10002  pjnormss 10007  pjclem4 10037  pjadj2co 10042  pj3s 10045  pj3 10046  hstnmoct 10060  hstle1t 10063  hst1ht 10064  hstlet 10067  hstoht 10069  spansncv2t 10130  dmdmdt 10137  mdslmd1lem2 10161  mdslmd2 10165  atcveq0 10183  chcv1t 10190  chcv2t 10191  cvexchlem 10203  cvp 10210  atcv1t 10215  atexcht 10216  atoml 10217  atcvatlem 10220  irredlem2 10226  irred 10229  atdmd 10233  atmd2 10235  mdsymlem3 10240  mdsymlem5 10242  sumdmdlem 10252  sumdmdlem2 10253  cdj1 10265  cdj3lem1 10266  cdj3lem2b 10269  cdj3 10273  symggrpiOLD 10311  symggrpi 10313  cayleylem2 10317  11st22nd 10354  cnfilca 10451  iint 10478

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