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 857  syl3anl 873  eupick 1427  vtocl2gf 1840  csbnest1g 2027  reuss2 2265  sonr 2846  sotr 2847  so2nr 2849  so3nr 2850  wecmpep 2931  wetrep 2932  wereu 2935  ordelss 2954  ordelord 2960  onelon 2962  ordin 2967  ordtri3or 2969  ordsssuc 3047  onmindif 3050  ordsucss 3059  ordsucelsuc 3063  ordunisssuc 3073  ordunisuc2 3105  limsssuc 3111  ordom 3131  limom 3136  nnsuc 3138  imadif 3560  fnbr 3576  fnex 3593  feu 3632  fex 3637  dffo2 3660  foco 3667  f1dmex 3695  ffoss 3696  funbrfv 3735  fvco 3759  fvopabg 3770  fvimacnvALT 3794  ffvelrn 3799  dffo4 3805  fopabco 3817  fsn2 3821  fvconst2g 3829  funfvima 3837  funiunfv 3851  f1ocnvfv1 3863  f1ocnvfv2 3864  f1ofveu 3867  f1ocnvfv3 3868  f1ocnvdm 3869  isocnv 3881  isotr 3882  isotrALT 3883  isomin 3884  isoini 3885  isowe 3888  f1oiso 3889  iinon 3895  tfrlem2 3897  tfrlem8 3903  tfrlem11 3906  rdglimt 3933  tz7.48lem 3940  curry1f 4083  oalimcl 4178  oaass 4179  omordi 4181  omword2 4189  omlimcl 4193  odi 4194  omass 4195  oen0 4197  oeordsuc 4205  oelim2 4206  nnaordex 4233  nnawordex 4234  oaabs 4236  ecoprass 4304  mapsn 4329  f1domg 4377  endomtr 4401  fundmen 4409  pw2en 4426  sdomdomtr 4449  mapenlem1 4469  mapenlem2 4470  mapxpen 4475  xpmapenlem4 4479  mapunen 4482  ssenen 4484  phplem1 4488  omsucdom 4502  sucdomi 4503  pssnn 4513  ssfi 4515  isfinite2 4523  unfilem1 4524  unifi 4532  fodomfib 4541  suppr 4562  supsnALT 4564  r1ord 4627  r1val1 4630  rankr1 4646  r1pwcl 4659  rankxplim3 4686  karden 4698  ac6lem 4726  ondomon 4828  ondomcard 4829  alephordi 4846  cardaleph 4857  carduniima 4862  cardinfima 4863  cflim 4881  addclpi 4992  addasspi 4995  mulasspi 4997  addnidpi 5000  ltexpq 5052  prub 5070  genpnnp 5080  genpass 5084  addclprlem1 5090  mulclprlem 5093  1idpr 5105  prlem934b 5110  prlem934 5111  ltexprlem4 5117  ltexprlem6 5119  ltexprlem7 5120  reclem3pr 5130  suplem2pr 5134  00sr 5180  mulgt0sr 5186  recexsr 5188  map2psrpr 5192  suppsr 5194  supsrlem6 5202  supre 5232  adddirt 5291  add4t 5310  cnegextlem3 5319  addsubasst 5355  addsub12t 5358  2addsubt 5361  negcon1t 5382  mul4t 5392  muladd11t 5394  subdirt 5400  negdi2t 5428  negsubdi2t 5430  neg2subt 5431  subsub4t 5436  subadd4t 5447  axsup 5479  eqlet 5544  le2tri3 5563  ltaddsubt 5605  leaddsubt 5607  ltnegcon1t 5629  lenegcon1t 5631  recext 5657  divasst 5704  p1let 5773  ltmul2t 5787  gt0divt 5807  ge0divt 5808  ltdivmult 5819  ledivmult 5820  ltrec1t 5836  lerec2t 5837  ltdiv23t 5840  lediv23t 5841  recgt1it 5848  nn2get 5890  nnltp1let 5902  suprleub 6006  nnunb 6017  xrsupsslem 6023  xrinfmsslem 6024  supxr2 6029  supxrre 6030  supxrunb1 6036  supxrbnd 6038  supxrleub 6046  nn0addclt 6067  elnnz1 6102  zaddclt 6112  elnnnn0b 6120  elnnnn0c 6121  zltp1let 6128  zlem1ltt 6130  gtndivt 6140  primet 6142  msqznn 6143  uzindOLD 6156  btwnz 6163  zmax 6168  zbtwnre 6169  rebtwnz 6170  flltt 6179  fladdzt 6187  ceilet 6193  qaddclt 6207  qrecclt 6211  qdivclt 6212  qbtwnre 6216  seq1rn 6259  seq1cl 6262  seq1cl2 6263  ser1add 6276  shftres 6281  shftval4t 6286  shftcan1t 6291  elioc2t 6322  elico2t 6323  elicc2t 6324  iccsupr 6331  uzss 6363  uzwo2 6389  elfz5t 6406  fzss1t 6435  fzssp1t 6438  fzp1sst 6439  fsequb 6455  fseqsupub 6458  seqzfveq 6486  expgt0t 6520  expgt1t 6523  mulexpt 6525  recexpt 6526  expmult 6528  expordit 6531  expmwordit 6537  exple1t 6538  expubndt 6539  bernneq 6583  expnbndt 6585  sqrlem5 6607  cjexpt 6752  absnidt 6798  absexpt 6803  abssubne0t 6820  absdifltt 6821  absdiflet 6822  lenegsqt 6823  seq1bnd 6847  seq1ublem 6848  cau3ir 6852  cau5i 6854  cvg3 6860  cvganz 6861  facdivt 6879  facndivt 6880  faclbnd3 6884  faclbnd5 6890  faclbnd6 6891  bccmplt 6900  bccl2t 6909  fsump1s 6951  fsumcllem 6952  fsum1ps 6956  fsumsplit 6958  fsumcom 6966  fsumrev 6967  fsumrev2 6968  fsumshftm 6970  fsummulc1 6971  fsumconst 6976  fsumcmpndx2 6980  fsumabs 6981  serz1p 6990  binomlem1 7004  bcxmas 7014  clm3 7017  climrecl 7047  climge0 7049  climaddlem3 7052  climaddc2 7055  climmullem4 7059  climmullem5 7060  climmullem8 7063  clim2serzt 7070  climcmpc1 7075  clim2serz 7081  climabslem 7084  climsup 7091  caucvglem2 7094  caucvglem5 7097  caucvglem6 7098  serzf0 7105  ser1f0 7106  ser1cmp2 7113  isum1p 7141  expcnv 7168  geoisumr 7178  cvgratlem2ALT 7183  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag4 7196  cncffvrn 7208  mulc1cncf 7214  ivthlem7 7222  ivthlem7OLD 7231  efexpt 7314  eftlclt 7321  reeftlclt 7322  abspef01tlub 7336  reeff1o 7368  cos01gt0 7419  demoivre 7426  demoivreALT 7427  ruclem13 7465  infxpidmlem1 7495  infxpidmlem7 7501  infxpidmlem10 7504  infxpidmlem11 7505  infxpidmlem12 7506  infcda 7510  infdif 7511  infmap2lem2 7522  tgss2t 7579  subtop 7588  iscld 7611  clsval 7619  clsval2 7627  clsndisj 7648  neival 7658  ssnei2 7671  opnneiss 7673  lpval 7684  cnco 7707  cnpco 7708  cncnplem4 7716  sncld 7726  metreslem 7762  metxp 7774  bl2in 7783  blssex 7794  ssblex 7796  opni3 7806  opnin 7809  lpbl 7819  metcnpf 7822  metcnplem 7825  metcnp 7826  metcnss 7837  metcnss2 7838  metidcn 7839  lmbr 7866  lmnn 7873  cmscvg 7882  lmss 7888  causs 7890  lmle 7895  lmclim 7898  metelcls 7900  xplmi 7907  xplm 7909  xpcn 7910  oprcn 7911  opr2cn 7913  iscms2lem4 7926  cmsss 7931  bcthlem16 7948  bcthlem17 7949  bcthlem24 7956  bcthlem25 7957  bcthlem30 7962  bcthlem33 7965  grpidinvlem3 7984  grpidinv 7986  grpidinv2 7994  abl23 8040  abl4 8041  ablmuldiv 8044  abldivdiv 8045  abldivdiv4 8046  ablnncan 8049  issubgi 8059  subgabl 8060  ghgrpilem3 8072  ghgrpilem4 8073  ring2 8086  ringaass 8091  ringa23 8092  ringrcan 8094  ringlcan 8095  ring0rid 8097  ring0lid 8098  vcid 8107  vcaass 8117  vca23 8118  vcrcan 8120  vclcan 8121  vc0rid 8123  vc0lid 8124  vcm 8127  vcrinv 8128  vclinv 8129  vcoprnelem 8135  nvass 8181  nvadd23 8183  nvrcan 8184  nvlcan 8185  nvsid 8188  nvsass 8189  nvdi 8191  nvdir 8192  nv2 8193  nv0rid 8196  nv0lid 8197  nv0 8198  nvsz 8199  nvinv 8200  invfval 8201  nvnnncan1 8208  nvnnncan2 8209  nvnegneg 8211  nvrinv 8213  nvlinv 8214  nvaddsubass 8218  nvaddsub 8219  nvcl 8227  nvmtri2 8239  nvelbl 8263  nvelbl2 8264  nvlmcl 8267  ipid 8297  sspg 8321  ssps 8323  sspmval 8326  sspn 8329  sspival 8331  sspimsval 8333  lnosub 8353  lnomul 8354  nvcnpi4 8355  nmoub3i 8368  nmounbi 8371  blometi 8394  ipasslem1 8421  ipasslem2 8422  ipasslem3 8423  ipasslem4 8424  ipasslem5 8425  ipasslem8 8428  ipdi 8434  ipassr 8437  ipsubdir 8439  ipsubdi 8440  sspph 8446  ubthlem3 8462  ubthlem5 8464  ubthlem6 8465  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  minveclem9 8484  minveclem25 8500  minveclem27 8502  minveclem28 8503  minveclem38 8513  hlass 8533  hladdid 8535  hlmulid 8537  hlmulass 8538  hldi 8539  hldir 8540  hlmul0 8541  hlipdir 8544  hlipass 8545  hlcompl 8547  htthlem5 8554  htthlem6 8555  htthlem8 8557  htthlem10 8559  efif1lem5 8649  circgrpOLD 8658  shftefif1olem 8661  shftefif1olemOLD 8662  explogt 8694  reexplogt 8695  relogexpt 8696  logexptOLD 8712  explogtOLD 8713  axgroth3 8718  h2hlm 8789  hvadd4t 8826  hvaddsubasst 8831  hvmulcan2t 8861  hiassdit 8878  hcau2 8976  hlim2 8981  hhcms 8993  hsn0elch 9041  norm1ex 9043  hhssnv 9054  hhsscms 9067  ocsh 9072  occllem6 9094  projlem21 9122  projlem25 9126  projlem26 9127  pjpjtht 9173  pjopt 9175  pjpot 9176  pjocclt 9181  shsel3t 9194  elspanclt 9220  chsscon1t 9339  chpsscon1t 9342  chdmm2t 9364  chdmj2t 9368  h1de2ctlem 9394  elspansnclt 9404  pjspansnt 9417  fh2t 9479  cm2jt 9480  osumlem1 9495  osumlem2 9496  spansncv 9514  5oalem2 9517  3oalem1 9524  pjot 9533  pjjs 9562  pjds 9574  pjds3 9575  pjoi0t 9579  hoadd4t 9627  homco1t 9644  homulasst 9645  hoadddit 9646  hoadddirt 9647  honegsubdi2t 9654  hosubadd4t 9657  hoaddsubasst 9658  hosubsub4t 9661  adjsymt 9676  cnvadj 9733  hhlno 9743  unopf1ot 9756  unopnormt 9757  cnvunopt 9758  unopadjt 9759  unoplint 9760  counopt 9761  hmopret 9763  adjclt 9772  adj2t 9774  hmoplint 9782  braclt 9789  kbopt 9793  kbmult 9795  eighmret 9803  eighmortht 9804  lnopmult 9807  lnopmulsub 9816  0lnfn 9825  lnopm 9840  lnophs 9841  lnopco 9843  nmopunt 9854  hmopst 9860  hmopmt 9861  hmopcot 9863  nmcopexlem3 9868  nmcopexlem5 9870  nmcopexlem6 9871  lnopcon 9878  nmcfnexlem3 9897  nmcfnexlem5 9899  nmcfnexlem6 9900  lnfncon 9905  nlelch 9909  riesz3 9910  cnlnadjlem2 9916  cnlnadjlem6 9920  cnlnadjlem7 9921  cnlnadjeu 9925  adjbdlnt 9931  adjlnopt 9934  adjmult 9939  adjaddt 9940  nmopco 9942  adjco 9947  nmopcoadj 9948  branmfnt 9951  cnvbramult 9960  kbass2t 9962  kbass5t 9965  leop2t 9969  leopsqt 9974  leopaddt 9977  leopmulit 9978  leopmult 9979  leopnmidt 9982  nmopleidt 9983  pjnmop 9986  hmopidmchlem 9989  hmopidmch 9990  pjadjco 10000  pjima 10015  pjadj2co 10042  stclt 10053  hstclt 10054  stadd 10083  strlem3 10090  strlem4 10091  strlem5 10092  hstrlem3 10098  hstrlem4 10099  hstrlem5 10100  cvcon3t 10121  mdbr2 10133  dmdmdt 10137  mddmd 10144  mdsl0 10145  mdsl3t 10151  mdslmd1lem1 10160  mdslmd4 10168  atsseq 10182  atcveq0 10183  ch1dle 10187  atom1d 10188  superpos 10189  shatomic 10193  shatomistic 10196  cvexchlem 10203  atnem0 10212  atcv0eq 10214  atord 10219  atcvatlem 10220  irredlem1 10225  irredlem2 10226  irredlem3 10227  atcvat3 10231  atdmd 10233  mdsymlem5 10242  sumdmdlem 10252  cdj3lem2 10267  symggrpiOLD 10311  symggrpi 10313  cayleylem2 10317  idmoa 10508  rcmob 10526  idosc 10546  dmo 10553  cdmo 10554  jdmo 10555  homib 10568  iri 10572

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