Theorem sylan 448

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan	|- ((th /\ ps) -> ch)

Proof of Theorem sylan

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sylanb 449  sylanbr 450  syl2an 454  sylanl1 460  sylanl2 461  syl3an1 858  syl3anl 874  eupick 1432  vtocl2gf 1845  csbnest1g 2033  reuss2 2271  sonr 2850  sotr 2851  so2nr 2853  so3nr 2854  wecmpep 2936  wetrep 2937  wereu 2940  ordelss 2959  ordelord 2965  onelon 2967  ordtri3or 2974  ordsssuc 3052  onmindif 3055  ordsucss 3064  ordsucelsuc 3068  ordunisssuc 3078  ordunisuc2 3110  limsssuc 3116  ordom 3136  limom 3141  nnsuc 3143  imadif 3566  fnbr 3582  fnex 3599  feu 3638  fex 3643  dffo2 3666  foco 3673  f1dmex 3701  ffoss 3702  funbrfv 3741  fvco 3765  fvopabg 3776  fvimacnvALT 3800  ffvelrn 3805  dffo4 3811  fopabco 3823  fsn2 3827  fvconst2g 3835  funfvima 3843  funiunfv 3857  f1ocnvfv1 3869  f1ocnvfv2 3870  f1ofveu 3873  f1ocnvfv3 3874  f1ocnvdm 3875  isocnv 3887  isotr 3888  isotrALT 3889  isomin 3890  isoini 3891  isowe 3894  f1oiso 3895  iinon 3901  tfrlem2 3903  tfrlem8 3909  tfrlem11 3912  tz7.48lem 3946  curry1f 4089  oalimcl 4184  oaass 4185  omordi 4187  omword2 4195  omlimcl 4199  odi 4200  omass 4201  oen0 4203  oeordsuc 4211  oelim2 4212  nnaordex 4239  nnawordex 4240  oaabs 4242  ecoprass 4310  mapsn 4335  f1domg 4383  endomtr 4407  fundmen 4415  pw2en 4432  sdomdomtr 4455  mapenlem1 4475  mapenlem2 4476  mapxpen 4481  xpmapenlem4 4485  mapunen 4488  ssenen 4490  phplem1 4494  omsucdom 4508  sucdomi 4509  pssnn 4519  ssfi 4521  isfinite2 4529  unfilem1 4530  unifi 4538  fodomfib 4547  suppr 4570  supsnALT 4572  r1ord 4635  r1val1 4638  rankr1 4654  r1pwcl 4667  rankxplim3 4694  karden 4706  ac6lem 4734  ondomon 4836  ondomcard 4837  alephordi 4854  cardaleph 4865  carduniima 4870  cardinfima 4871  cflim 4889  addclpi 5000  addasspi 5003  mulasspi 5005  addnidpi 5008  ltexpq 5060  prub 5078  genpnnp 5088  genpass 5092  addclprlem1 5098  mulclprlem 5101  1idpr 5113  prlem934b 5118  prlem934 5119  ltexprlem4 5125  ltexprlem6 5127  ltexprlem7 5128  reclem3pr 5138  suplem2pr 5142  00sr 5188  mulgt0sr 5194  recexsr 5196  map2psrpr 5200  suppsr 5202  supsrlem6 5210  supre 5240  adddirt 5299  add4t 5318  cnegextlem3 5327  addsubasst 5363  addsub12t 5366  2addsubt 5369  negcon1t 5390  mul4t 5400  muladd11t 5402  subdirt 5408  negdi2t 5436  negsubdi2t 5438  neg2subt 5439  subsub4t 5444  subadd4t 5455  axsup 5487  eqlet 5552  le2tri3 5571  ltaddsubt 5613  leaddsubt 5615  ltnegcon1t 5637  lenegcon1t 5639  recext 5665  divasst 5712  p1let 5781  ltmul2t 5795  gt0divt 5815  ge0divt 5816  ltdivmult 5827  ledivmult 5828  ltrec1t 5844  lerec2t 5845  ltdiv23t 5848  lediv23t 5849  nn2get 5898  nnltp1let 5910  suprleub 6014  nnunb 6025  xrsupsslem 6031  xrinfmsslem 6032  supxr2 6037  supxrre 6038  supxrunb1 6044  supxrbnd 6046  supxrleub 6054  nn0addclt 6075  elnnz1 6110  zaddclt 6120  elnnnn0b 6128  elnnnn0c 6129  zltp1let 6136  zlem1ltt 6138  gtndivt 6148  primet 6150  msqznn 6151  uzindOLD 6164  btwnz 6171  zmax 6176  zbtwnre 6177  rebtwnz 6178  flltt 6187  fladdzt 6195  ceilet 6201  qaddclt 6215  qrecclt 6219  qdivclt 6220  qbtwnre 6224  seq1rn 6267  seq1cl 6270  seq1cl2 6271  ser1add 6284  shftres 6289  shftval4t 6294  shftcan1t 6299  elioc2t 6330  elico2t 6331  elicc2t 6332  iccsupr 6339  uzss 6371  uzwo2 6397  elfz5t 6414  fzss1t 6443  fzssp1t 6446  fzp1sst 6447  fsequb 6463  fseqsupub 6466  seqzfveq 6494  expgt0t 6528  expgt1t 6531  mulexpt 6533  recexpt 6534  expmult 6536  expordit 6539  expmwordit 6545  exple1t 6546  expubndt 6547  bernneq 6591  expnbndt 6593  sqrlem5 6615  cjexpt 6760  absnidt 6806  absexpt 6811  abssubne0t 6828  absdifltt 6829  absdiflet 6830  lenegsqt 6831  seq1bnd 6855  seq1ublem 6856  cau3ir 6860  cau5i 6862  cvg3 6868  cvganz 6869  facdivt 6887  facndivt 6888  faclbnd3 6892  faclbnd5 6898  faclbnd6 6899  bccmplt 6908  bccl2t 6917  fsump1s 6959  fsumcllem 6960  fsum1ps 6964  fsumsplit 6966  fsumcom 6974  fsumrev 6975  fsumrev2 6976  fsumshftm 6978  fsummulc1 6979  fsumconst 6984  fsumcmpndx2 6988  fsumabs 6989  serz1p 6998  binomlem1 7012  bcxmas 7022  clm3 7025  climrecl 7055  climge0 7057  climaddlem3 7060  climaddc2 7063  climmullem4 7067  climmullem5 7068  climmullem8 7071  clim2serzt 7078  climcmpc1 7083  clim2serz 7089  climabslem 7092  climsup 7099  caucvglem2 7102  caucvglem5 7105  caucvglem6 7106  serzf0 7113  ser1f0 7114  ser1cmp2 7121  isum1p 7149  expcnv 7176  geoisumr 7186  cvgratlem2ALT 7191  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag2 7202  fsum0diag4 7204  cncffvrn 7216  mulc1cncf 7222  ivthlem7 7230  ivthlem7OLD 7239  efexpt 7322  eftlclt 7329  reeftlclt 7330  abspef01tlub 7344  reeff1o 7376  cos01gt0 7427  demoivre 7434  demoivreALT 7435  ruclem13 7473  infxpidmlem1 7503  infxpidmlem7 7509  infxpidmlem10 7512  infxpidmlem11 7513  infxpidmlem12 7514  infcda 7518  infdif 7519  infmap2lem2 7530  tgss2t 7587  subtop 7596  iscld 7619  clsval 7627  clsval2 7635  clsndisj 7656  neival 7667  ssnei2 7680  opnneiss 7682  lpval 7693  cnco 7718  cnpco 7719  cncnplem4 7727  sncld 7737  metreslem 7774  metxp 7786  bl2in 7795  blssex 7806  ssblex 7808  opni3 7818  opnin 7821  lpbl 7832  metcnpf 7835  metcnplem 7838  metcnp 7839  metcnss 7850  metcnss2 7851  metidcn 7852  lmbr 7880  lmnn 7887  cmscvg 7898  lmss 7904  causs 7906  lmle 7911  lmclim 7914  metelcls 7916  xplmi 7923  xplm 7925  xpcn 7926  oprcn 7927  opr2cn 7929  iscms2lem4 7942  cmsss 7947  bcthlem16 7964  bcthlem17 7965  bcthlem24 7972  bcthlem25 7973  bcthlem30 7978  bcthlem33 7981  grpidinvlem3 8000  grpidinv 8002  grpidinv2 8010  abl23 8055  abl4 8056  ablmuldiv 8059  abldivdiv 8060  abldivdiv4 8061  ablnncan 8064  issubgi 8074  subgabl 8075  ghgrpilem3 8087  ghgrpilem4 8088  ring2 8101  ringaass 8106  ringa23 8107  ringrcan 8109  ringlcan 8110  ring0rid 8112  ring0lid 8113  vcid 8122  vcaass 8132  vca23 8133  vcrcan 8135  vclcan 8136  vc0rid 8138  vc0lid 8139  vcm 8142  vcrinv 8143  vclinv 8144  vcoprnelem 8149  nvass 8193  nvadd23 8195  nvrcan 8196  nvlcan 8197  nvsid 8200  nvsass 8201  nvdi 8203  nvdir 8204  nv2 8205  nv0rid 8208  nv0lid 8209  nv0 8210  nvsz 8211  nvinv 8212  invfval 8213  nvnnncan1 8220  nvnnncan2 8221  nvnegneg 8223  nvrinv 8225  nvlinv 8226  nvaddsubass 8230  nvaddsub 8231  nvcl 8239  nvmtri2 8252  nvelbl 8276  nvelbl2 8277  nvlmcl 8280  ipid 8310  sspg 8334  ssps 8336  sspmval 8339  sspn 8342  sspival 8344  sspimsval 8346  lnosub 8366  lnomul 8367  nvcnpi4 8368  nmoub3i 8381  nmounbi 8384  blometi 8407  ipasslem1 8434  ipasslem2 8435  ipasslem3 8436  ipasslem4 8437  ipasslem5 8438  ipasslem8 8441  ipdi 8447  ipassr 8450  ipsubdir 8452  ipsubdi 8453  sspph 8459  ubthlem3 8475  ubthlem5 8477  ubthlem6 8478  ubthlem9 8481  ubthlem10 8482  ubthlem11 8483  minveclem9 8497  minveclem25 8513  minveclem27 8515  minveclem28 8516  minveclem38 8526  hlass 8546  hladdid 8548  hlmulid 8550  hlmulass 8551  hldi 8552  hldir 8553  hlmul0 8554  hlipdir 8557  hlipass 8558  hlcompl 8560  htthlem5 8567  htthlem6 8568  htthlem8 8570  htthlem10 8572  pstr 8594  efif1lem5 8668  circgrpOLD 8677  shftefif1olem 8680  explogt 8711  reexplogt 8712  relogexpt 8713  axgroth3 8718  h2hlm 8789  hvadd4t 8844  hvaddsubasst 8849  hvmulcan2t 8879  hiassdit 8896  hcau2 8994  hlim2 8999  hhcms 9011  hsn0elch 9059  norm1ex 9061  hhssnv 9073  hhsscms 9089  ocsh 9095  occllem6 9117  projlem21 9145  projlem25 9149  projlem26 9150  pjpjtht 9196  pjopt 9198  pjpot 9199  pjocclt 9204  shsel3t 9217  elspanclt 9243  chsscon1t 9362  chpsscon1t 9365  chdmm2t 9387  chdmj2t 9391  h1de2ctlem 9417  elspansnclt 9427  pjspansnt 9440  fh2t 9502  cm2jt 9503  osumlem1 9518  osumlem2 9519  spansncv 9537  5oalem2 9540  3oalem1 9547  pjot 9556  pjjs 9585  pjds 9597  pjds3 9598  pjoi0t 9602  hoadd4t 9650  homco1t 9667  homulasst 9668  hoadddit 9669  hoadddirt 9670  honegsubdi2t 9677  hosubadd4t 9680  hoaddsubasst 9681  hosubsub4t 9684  adjsymt 9699  cnvadj 9756  hhlno 9766  unopf1ot 9779  unopnormt 9780  cnvunopt 9781  unopadjt 9782  unoplint 9783  counopt 9784  hmopret 9786  adjclt 9795  adj2t 9797  hmoplint 9805  braclt 9812  kbopt 9816  kbmult 9818  eighmret 9826  eighmortht 9827  lnopmult 9830  lnopmulsub 9839  0lnfn 9848  lnopm 9863  lnophs 9864  lnopco 9866  nmopunt 9877  hmopst 9883  hmopmt 9884  hmopcot 9886  nmcopexlem3 9891  nmcopexlem5 9893  nmcopexlem6 9894  lnopcon 9901  nmcfnexlem3 9920  nmcfnexlem5 9922  nmcfnexlem6 9923  lnfncon 9928  nlelch 9932  riesz3 9933  cnlnadjlem2 9939  cnlnadjlem6 9943  cnlnadjlem7 9944  cnlnadjeu 9948  adjbdlnt 9954  adjlnopt 9957  adjmult 9963  adjaddt 9964  nmopco 9966  adjco 9971  nmopcoadj 9972  branmfnt 9976  cnvbramult 9986  kbass2t 9988  kbass5t 9991  leop2t 9995  leopsqt 10000  leopaddt 10003  leopmulit 10004  leopmult 10005  leopnmidt 10009  nmopleidt 10010  pjnmop 10013  hmopidmchlem 10016  hmopidmch 10017  pjadjco 10027  pjima 10042  pjadj2co 10070  stclt 10081  hstclt 10082  stadd 10111  strlem3 10118  strlem4 10119  strlem5 10120  hstrlem3 10126  hstrlem4 10127  hstrlem5 10128  cvcon3t 10149  mdbr2 10161  dmdmdt 10165  mddmd 10173  mdsl0 10174  mdsl3t 10180  mdslmd1lem1 10189  mdslmd4 10197  atsseq 10211  atcveq0 10212  ch1dle 10216  atom1d 10217  superpos 10218  shatomic 10222  shatomistic 10225  cvexchlem 10232  atnem0 10241  atcv0eq 10243  atord 10248  atcvatlem 10249  irredlem1 10254  irredlem2 10255  irredlem3 10256  atcvat3 10260  atdmd 10262  mdsymlem5 10271  sumdmdlem 10281  cdj3lem2 10296  symggrpi 10340  cayleylem2 10344  idmoa 10544  rcmob 10562  idosc 10582  dmo 10589  cdmo 10590  jdmo 10591  homib 10604  iri 10608

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