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 856  syl3anl 872  eupick 1411  vtocl2gf 1824  csbnest1g 2008  reuss2 2246  sonr 2819  sotr 2820  so2nr 2822  so3nr 2823  wecmpep 2904  wetrep 2905  wereu 2908  ordelss 2927  ordelord 2933  onelon 2935  ordin 2940  ordtri3or 2942  ordsssuc 3020  onmindif 3023  ordsucss 3032  ordsucelsuc 3036  ordunisssuc 3046  ordunisuc2 3078  limsssuc 3084  ordom 3104  limom 3109  nnsuc 3111  imadif 3514  fnbr 3530  fnex 3547  feu 3586  fex 3591  dffo2 3614  foco 3621  f1dmex 3649  ffoss 3650  funbrfv 3689  fvco 3713  fvopabg 3724  fvimacnvALT 3748  ffvelrn 3753  dffo4 3759  fopabco 3771  fsn2 3775  fvconst2g 3783  funfvima 3791  funiunfv 3805  f1ocnvfv1 3817  f1ocnvfv2 3818  f1ofveu 3821  f1ocnvfv3 3822  f1ocnvdm 3823  isocnv 3835  isotr 3836  isotrALT 3837  isomin 3838  isoini 3839  isowe 3842  f1oiso 3843  iinon 3849  tfrlem2 3851  tfrlem8 3857  tfrlem11 3860  rdglimt 3887  tz7.48lem 3894  curry1f 4037  oalimcl 4132  oaass 4133  omordi 4135  omword2 4143  omlimcl 4147  odi 4148  omass 4149  oen0 4151  oeordsuc 4159  oelim2 4160  nnaordex 4187  nnawordex 4188  oaabs 4190  ecoprass 4258  mapsn 4283  f1domg 4331  endomtr 4355  fundmen 4363  pw2en 4380  sdomdomtr 4403  mapenlem1 4421  mapenlem2 4422  mapxpen 4427  xpmapenlem4 4431  mapunen 4434  ssenen 4436  phplem1 4440  omsucdom 4454  sucdomi 4455  pssnn 4465  ssfi 4467  isfinite2 4475  unfilem1 4476  unifi 4484  fodomfib 4493  suppr 4514  supsnALT 4516  r1ord 4579  r1val1 4582  rankr1 4598  r1pwcl 4611  rankxplim3 4638  karden 4650  ac6lem 4678  ondomon 4779  ondomcard 4780  alephordi 4797  cardaleph 4808  carduniima 4813  cardinfima 4814  cflim 4832  addclpi 4943  addasspi 4946  mulasspi 4948  addnidpi 4951  ltexpq 5003  prub 5021  genpnnp 5031  genpass 5035  addclprlem1 5041  mulclprlem 5044  1idpr 5056  prlem934b 5061  prlem934 5062  ltexprlem4 5068  ltexprlem6 5070  ltexprlem7 5071  reclem3pr 5081  suplem2pr 5085  00sr 5131  mulgt0sr 5137  recexsr 5139  map2psrpr 5143  suppsr 5145  supsrlem6 5153  supre 5183  adddirt 5242  add4t 5261  cnegextlem3 5270  addsubasst 5306  addsub12t 5309  2addsubt 5312  negcon1t 5333  mul4t 5343  muladd11t 5345  subdirt 5351  negdi2t 5379  negsubdi2t 5381  neg2subt 5382  subsub4t 5387  subadd4t 5398  axsup 5430  eqlet 5495  le2tri3 5514  ltaddsubt 5556  leaddsubt 5558  ltnegcon1t 5580  lenegcon1t 5582  recext 5608  divasst 5655  p1let 5724  ltmul2t 5738  gt0divt 5758  ge0divt 5759  ltdivmult 5770  ledivmult 5771  ltrec1t 5787  lerec2t 5788  ltdiv23t 5791  lediv23t 5792  recgt1it 5799  nn2get 5841  nnltp1let 5853  suprleub 5957  nnunb 5968  xrsupsslem 5974  xrinfmsslem 5975  supxr2 5980  supxrre 5981  supxrunb1 5987  supxrbnd 5989  supxrleub 5997  nn0addclt 6018  elnnz1 6053  zaddclt 6063  elnnnn0b 6071  elnnnn0c 6072  zltp1let 6079  zlem1ltt 6081  gtndivt 6091  primet 6093  msqznn 6094  uzindOLD 6107  btwnz 6114  zmax 6119  zbtwnre 6120  rebtwnz 6121  flltt 6130  fladdzt 6138  ceilet 6144  qaddclt 6158  qrecclt 6162  qdivclt 6163  qbtwnre 6167  seq1rn 6210  seq1cl 6213  seq1cl2 6214  ser1add 6227  shftres 6232  shftval4t 6237  shftcan1t 6242  elioc2t 6273  elico2t 6274  elicc2t 6275  iccsupr 6282  uzss 6314  uzwo2 6340  elfz5t 6357  fzss1t 6386  fzssp1t 6389  fzp1sst 6390  fsequb 6406  fseqsupub 6409  seqzfveq 6437  expgt0t 6471  expgt1t 6474  mulexpt 6476  recexpt 6477  expmult 6479  expordit 6482  expmwordit 6488  exple1t 6489  expubndt 6490  bernneq 6534  expnbndt 6536  sqrlem5 6558  cjexpt 6703  absnidt 6749  absexpt 6754  abssubne0t 6771  absdifltt 6772  absdiflet 6773  lenegsqt 6774  seq1bnd 6798  seq1ublem 6799  cau3ir 6803  cau5i 6805  cvg3 6811  cvganz 6812  facdivt 6830  facndivt 6831  faclbnd3 6835  faclbnd5 6841  faclbnd6 6842  bccmplt 6851  bccl2t 6860  fsump1s 6902  fsumcllem 6903  fsum1ps 6907  fsumsplit 6909  fsumcom 6917  fsumrev 6918  fsumrev2 6919  fsumshftm 6921  fsummulc1 6922  fsumconst 6927  fsumcmpndx2 6931  fsumabs 6932  serz1p 6941  binomlem1 6955  bcxmas 6965  clm3 6968  climrecl 6998  climge0 7000  climaddlem3 7003  climaddc2 7006  climmullem4 7010  climmullem5 7011  climmullem8 7014  clim2serzt 7021  climcmpc1 7026  clim2serz 7032  climabslem 7035  climsup 7042  caucvglem2 7045  caucvglem5 7048  caucvglem6 7049  serzf0 7056  ser1f0 7057  ser1cmp2 7064  isum1p 7092  expcnv 7119  geoisumr 7129  cvgratlem2ALT 7134  cvgratlem5 7140  fsum0diaglem2 7143  fsum0diag2 7145  fsum0diag4 7147  cncffvrn 7159  mulc1cncf 7165  ivthlem7 7173  ivthlem7OLD 7182  efexpt 7265  eftlclt 7272  reeftlclt 7273  abspef01tlub 7287  reeff1o 7319  cos01gt0 7370  demoivre 7377  demoivreALT 7378  ruclem13 7416  infxpidmlem1 7446  infxpidmlem7 7452  infxpidmlem10 7455  infxpidmlem11 7456  infxpidmlem12 7457  infcda 7461  infdif 7462  infmap2lem2 7473  tgss2t 7530  subtop 7539  iscld 7562  clsval 7570  clsval2 7578  clsndisj 7598  neival 7606  ssnei2 7619  opnneiss 7621  lpval 7632  cnco 7655  cnpco 7656  cncnplem4 7664  sncld 7674  metreslem 7710  metxp 7722  bl2in 7731  blssex 7742  ssblex 7744  opni3 7754  opnin 7757  lpbl 7767  metcnpf 7770  metcnplem 7773  metcnp 7774  metcnss 7785  metcnss2 7786  metidcn 7787  lmbr 7814  lmnn 7821  cmscvg 7830  lmss 7836  causs 7838  lmle 7843  lmclim 7846  metelcls 7848  xplmi 7855  xplm 7857  xpcn 7858  oprcn 7859  opr2cn 7861  iscms2lem4 7874  cmsss 7879  bcthlem16 7896  bcthlem17 7897  bcthlem24 7904  bcthlem25 7905  bcthlem30 7910  bcthlem33 7913  grpidinvlem3 7932  grpidinv 7934  grpidinv2 7942  abl23 7988  abl4 7989  ablmuldiv 7992  abldivdiv 7993  abldivdiv4 7994  ablnncan 7997  issubgi 8007  subgabl 8008  ghgrpilem3 8020  ghgrpilem4 8021  ring2 8034  ringaass 8039  ringa23 8040  ringrcan 8042  ringlcan 8043  ring0rid 8045  ring0lid 8046  vcid 8057  vcaass 8067  vca23 8068  vcrcan 8070  vclcan 8071  vc0rid 8073  vc0lid 8074  vcm 8077  vcrinv 8078  vclinv 8079  nvass 8119  nvadd23 8121  nvrcan 8122  nvlcan 8123  nvsid 8126  nvsass 8127  nvdi 8129  nvdir 8130  nv2 8131  nv0rid 8134  nv0lid 8135  nv0 8136  nvsz 8137  nvinv 8138  nvnnncan1 8145  nvnnncan2 8146  nvnegneg 8148  nvrinv 8150  nvlinv 8151  nvaddsubass 8155  nvaddsub 8156  nvcl 8164  nvmtri2 8176  nvelbl 8200  nvelbl2 8201  nvlmcl 8204  ipid 8232  sspg 8256  ssps 8258  sspmval 8261  sspn 8264  sspival 8266  sspimsval 8268  lnosub 8288  lnomul 8289  nvcnpi4 8290  nmoub3i 8303  nmounbi 8306  blometi 8329  ipasslem1 8356  ipasslem2 8357  ipasslem3 8358  ipasslem4 8359  ipasslem5 8360  ipasslem8 8363  ipdi 8369  ipassr 8372  ipsubdir 8374  ipsubdi 8375  sspph 8381  ubthlem3 8397  ubthlem5 8399  ubthlem6 8400  ubthlem9 8403  ubthlem10 8404  ubthlem11 8405  minveclem9 8419  minveclem25 8435  minveclem27 8437  minveclem28 8438  minveclem38 8448  hlass 8467  hladdid 8469  hlmulid 8471  hlmulass 8472  hldi 8473  hldir 8474  hlmul0 8475  hlipdir 8478  hlipass 8479  hlcompl 8481  htthlem5 8488  htthlem6 8489  htthlem8 8491  htthlem10 8493  efif1lem5 8562  circgrpOLD 8571  shftefif1olem 8574  shftefif1olemOLD 8575  explogt 8607  reexplogt 8608  relogexpt 8609  logexptOLD 8625  explogtOLD 8626  axgroth3 8631  symggrpi 8673  cayleylem2 8677  idmoa 8858  rcmob 8876  idosc 8896  dmo 8903  cdmo 8904  jdmo 8905  homib 8918  iri 8922  hvadd4t 9054  hvaddsubasst 9059  hvmulcan2t 9089  hiassdit 9106  hcau2 9205  hlim2 9211  hillim 9216  hhcms 9223  hsn0elch 9271  norm1ex 9273  ocsh 9286  occllem6 9308  projlem21 9336  projlem25 9340  projlem26 9341  pjpjtht 9387  pjopt 9389  pjpot 9390  pjocclt 9395  shsel3t 9408  elspanclt 9434  chsscon1t 9553  chpsscon1t 9556  chdmm2t 9578  chdmj2t 9582  h1de2ctlem 9608  elspansnclt 9618  pjspansnt 9631  fh2t 9693  cm2jt 9694  osumlem1 9709  osumlem2 9710  spansncv 9728  5oalem2 9731  3oalem1 9738  pjot 9747  pjjs 9776  pjds 9788  pjds3 9789  pjoi0t 9793  hoadd4t 9841  homco1t 9858  homulasst 9859  hoadddit 9860  hoadddirt 9861  honegsubdi2t 9868  hosubadd4t 9871  hoaddsubasst 9872  hosubsub4t 9875  adjsymt 9890  cnvadj 9947  hhlno 9957  unopf1ot 9970  unopnormt 9971  cnvunopt 9972  unopadjt 9973  unoplint 9974  counopt 9975  hmopret 9977  adjclt 9986  adj2t 9988  hmoplint 9996  braclt 10003  kbopt 10007  kbmult 10009  eighmret 10017  eighmortht 10018  lnopmult 10021  lnopmulsub 10030  0lnfn 10039  lnopm 10054  lnophs 10055  lnopco 10057  nmopunt 10068  hmopst 10074  hmopmt 10075  hmopcot 10077  nmcopexlem3 10082  nmcopexlem5 10084  nmcopexlem6 10085  lnopcon 10092  nmcfnexlem3 10111  nmcfnexlem5 10113  nmcfnexlem6 10114  lnfncon 10119  nlelch 10123  riesz3 10124  cnlnadjlem2 10130  cnlnadjlem6 10134  cnlnadjlem7 10135  cnlnadjeu 10139  adjbdlnt 10145  adjlnopt 10148  adjmult 10153  adjaddt 10154  nmopco 10156  adjco 10161  nmopcoadj 10162  branmfnt 10165  cnvbramult 10174  kbass2t 10176  kbass5t 10179  leop2t 10183  leopsqt 10188  leopaddt 10191  leopmulit 10192  leopmult 10193  leopnmidt 10196  nmopleidt 10197  pjnmop 10200  hmopidmchlem 10203  hmopidmch 10204  pjadjco 10214  pjima 10229  pjadj2co 10256  stclt 10267  hstclt 10268  stadd 10297  strlem3 10304  strlem4 10305  strlem5 10306  hstrlem3 10312  hstrlem4 10313  hstrlem5 10314  cvcon3t 10335  mdbr2 10347  dmdmdt 10351  mddmd 10358  mdsl0 10359  mdsl3t 10365  mdslmd1lem1 10374  mdslmd4 10382  atsseq 10396  atcveq0 10397  ch1dle 10401  atom1d 10402  superpos 10403  shatomic 10407  shatomistic 10410  cvexchlem 10417  atnem0 10426  atcv0eq 10428  atord 10433  atcvatlem 10434  irredlem1 10439  irredlem2 10440  irredlem3 10441  atcvat3 10445  atdmd 10447  mdsymlem5 10456  sumdmdlem 10466  cdj3lem2 10481

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