Theorem sylan2 453

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 371	. . 3 |- (ph -> (ps -> ch))
3		sylan2.2	. . 3 |- (th -> ps)
4	2, 3	syl5 21	. 2 |- (ph -> (th -> ch))
5	4	imp 348	1 |- ((ph /\ th) -> ch)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  sylan2b 454  sylan2br 455  syl2an 456  sylanr1 464  sylanr2 465  ax11indalem 1407  ax11inda2ALT 1408  elabgt 1941  sbciegft 2007  hbsbc1gd 2031  hbsbcgd 2032  hbcsb1gd 2078  hbcsbgd 2079  csbnestg 2088  sbcnestg 2090  sspr 2540  ssiun 2660  trssord 2992  ordelssne 3002  onsssuc 3059  uniexb 3130  onint 3152  onint0 3153  onnmin 3160  onsucmin 3177  ordsucun 3180  nlimsucg 3196  ordunisuc2 3198  tfindsg 3213  tfindsg2 3214  peano5 3241  findsg 3245  cnvexg 3624  coexg 3629  funimass2 3678  cofunexg 3686  cofunex2g 3687  dmfex 3762  resdif 3816  funbrfv 3861  eqfnfv 3909  fvimacnvi 3918  fvimacnvALT 3923  funiunfv 3980  isofrlem 4015  fnotoprb 4049  foprrn 4096  fnoprvrn 4099  tfrlem8 4219  tfrlem9 4220  tfrlem11 4222  tfr3 4227  oasuc 4299  omsuc 4301  oalim 4303  omlim 4304  oalimcl 4330  oaass 4331  omlimcl 4345  odi 4346  omass 4347  oneo 4348  oelim2 4358  oeoelem 4361  nnaordex 4389  nnawordex 4390  oaabslem 4391  ecoprass 4461  ecoprdi 4462  mapex 4469  f1oen2g 4535  f1oeng 4536  domentr 4562  undom 4579  ac6sfilem3 4590  ac6sfi 4591  pwuninel 4631  mapunen 4649  ssenen 4651  phplem3 4657  phplem4 4658  php 4660  php3 4662  onomeneq 4665  omsucdom 4669  ssfi 4683  unbnn2 4691  unfi 4697  unifi 4701  fodomfi 4709  iunfi 4712  pm54.43 4715  supmaxlem 4731  omex 4772  aceq3 4879  aceq5 4886  aceq6b 4888  ac5b 4899  zorn2lem3 4936  imadomg 4952  sucdom 4992  ondomon 5006  alephnbtwn 5018  alephordi 5024  alephval2 5052  cfom 5066  axrepndlem2 5099  axpowndlem4 5106  axinfndlem1 5111  axacndlem5 5117  addclpi 5174  addasspi 5177  mulasspi 5179  distrpi 5180  mulcanpi 5181  indpi 5188  ltapq 5230  ltrpq 5239  prcdpq 5251  genpass 5266  distrlem1pr 5281  distrlem2pr 5282  distrlem4pr 5284  psslinpr 5289  prlem934b 5292  ltexprlem6 5301  ltexprlem7 5302  prlem936b 5308  prlem936 5309  reclem3pr 5312  reclem4pr 5313  recexsrlem 5366  suppsr3 5378  pre-axsup 5445  cnegexlem1 5499  cnegexlem3 5501  cnegex 5502  subneg 5548  subdi 5581  1re 5589  resubcl 5592  mulneg2 5606  negsubdi 5611  submul2 5614  subsub2 5615  nnncan1 5621  addsub4 5627  xrre 5723  le2tri3i 5743  ltaddsub 5785  leaddsub 5787  lenegcon2 5813  recextlem1 5838  recextlem2 5839  recex 5840  div12 5890  divneg 5913  letrp1 5956  lt2mul2div 6016  lerec2 6034  ledivdiv 6035  ltdiv23 6037  lediv23 6038  lediv12a 6041  ledivp1 6050  nndivre 6097  nndiv 6105  nndivtr 6106  rerpdivcl 6210  lble 6215  sup2 6219  dfinfmr 6235  nnunb 6238  arch 6239  bndndx 6241  xrsupsslem 6244  xrinfmsslem 6245  supxrunb1 6257  nn0ge0 6285  nn0addcl 6288  nn0leltp1 6296  nn0addge1 6298  nn0addge2 6299  zaddcl 6333  zsubcl 6336  zrevaddcl 6338  elnn0nn 6339  zltp1le 6349  zleltp1 6350  zltlem1 6352  zdiv 6356  peano2uz2 6372  uzind 6376  uzindOLD 6379  uzwo4OLD 6381  uzwo3lem1 6388  zmax 6392  zbtwnre 6393  rebtwnz 6394  qaddcl 6408  qsubcl 6411  qreccl 6412  qdivcl 6413  qrevaddcl 6414  irradd 6416  irrmul 6417  qbtwnre 6418  qsqueeze 6420  flge 6431  flwordi 6436  flbi 6439  fladdz 6443  modid 6471  modcyc 6475  modcyc2 6476  modmul1 6478  elioc2 6516  elico2 6517  elicc2 6518  icounlem 6539  eluzp1l 6561  uzwo 6582  uzwoOLD 6583  fzss2 6634  fzsuc 6636  fzrev2 6643  fzrev3i 6646  fzrevral 6650  fsequb 6654  fsequb2 6655  fseqsupubi 6657  seq1rn2 6686  ser1recli 6696  seqzp1 6743  seqzval2 6748  seqzeq 6750  seqzrn2 6751  seqzrn 6752  ser0cl1i 6759  expnnval 6767  expp1 6769  expm1t 6778  expeq0 6780  expge0 6785  expgt1 6786  expge1 6787  bernneq 6849  bernneqOLD 6850  expnlbnd 6853  expnlbnd2 6854  digit1 6856  replim 6962  mulre 6978  resub 7007  imsub 7010  cjsub 7017  sqabsadd 7050  sqabssub 7051  seq1bndi 7113  cau3iri 7118  cau5ii 7120  cvg2i 7125  faccl 7143  facdiv 7145  faclbnd4lem3 7153  faclbnd4lem4 7154  faclbnd5 7156  bccmpl 7165  fsum1s 7212  fsump1s 7216  fsum1ps 7221  fsumsplit 7223  fsumadd 7225  fsumcom 7231  fsumrev 7232  fsumshft 7234  fsummulc1 7236  fsummulc2 7237  fsum2mul 7240  fsumconst 7241  fsumcmp 7243  fsumcmp0 7244  fsumcmpndx2 7245  fsumabs 7246  fsumabs2mul 7247  serzcl2 7252  serzcmp0 7258  binomlem1 7269  binomlem2 7270  binomlem5 7273  binomlem6 7274  clm4i 7283  clm4lei 7284  clm4fi 7285  clm4a 7293  climfnn 7295  2climnn 7305  2climnn0 7306  iserzshft2i 7310  climge0 7315  climaddlem3 7319  climaddc1 7321  climmullem3 7325  climmullem5 7327  climmullem8 7330  climmulc2 7332  climsubc2 7334  clim2serz 7337  iserzmulc1 7339  iserzcmp 7345  clim2serzi 7348  climserzlei 7350  climsupi 7358  caucvglem6 7365  isumrecl 7414  expcnv 7437  explecnv 7438  geoisum1c 7450  cvgratlem1ALT 7452  cvgratlem2ALT 7453  cvgratlem1 7455  cvgratlem2 7456  cvgratlem4 7458  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag 7463  fsum0diag2 7464  mulc1cncf 7484  ivthlem7 7492  efcltlem1 7509  erelem1 7524  erelem3 7526  efaddlem5 7547  efaddlem6 7548  efsub 7576  efexp 7577  reeftlcl 7585  sinsub 7663  cossub 7664  demoivreALT 7696  acdc4lem1 7699  acdc5lem1 7703  acdcALT 7708  znnenlem 7713  unbenlem 7716  ruclem13 7734  infxpidmlem1 7764  infxpidmlem8 7771  infxpidmlem11 7774  infxpidmlem12 7775  infdif 7780  iunopn 7811  istps3 7820  eltg 7830  eltg2 7831  tgcl 7836  tgval3 7837  basgen2 7851  bastop1 7854  subbas2 7857  clsval2 7895  ntrss 7898  isnei 7928  isneip 7930  neips 7937  islp2 7957  iscncl 7980  metreslem 8032  blin 8062  blss 8063  isopn4 8072  opnin 8079  metequiv 8091  metcnpi3 8103  metcnpi4 8104  metcni2 8106  metcnss 8109  metcnss2 8110  lmbr 8139  lmnn 8146  lmuni 8162  causs 8166  lmfexlem2 8168  metelcls 8176  metcnp4 8181  xplmi2 8185  opr1cn 8189  lmcau 8207  bcthlem1 8210  bcthlem9 8218  bcthlem10 8219  bcthlem14 8223  bcthlem16 8225  bcthlem21 8230  grpidinvlem1 8261  grpidinvlem2 8262  grpideu 8266  gxadd 8331  gxnn0mul 8333  resgrprn 8336  grplactfval 8337  ablnncan 8353  issubgi 8364  ablmul 8372  ghgrpilem4 8377  isvc 8447  isnv 8478  nvmul0or 8519  imsmetlem 8570  nvcni3 8578  nvlmle 8580  vacnlem3 8584  nmcnilem 8591  sm1cnilem 8601  ipcl 8619  ip1cnilem2 8628  ip1cnilem3 8629  ip1cnilem5 8631  ip1cnilem6 8632  sspival 8651  lnocoi 8672  nmosetre 8681  nmoge0 8684  nmoub3i 8690  nmobndi 8692  nmlno0lem 8708  blo3i 8717  blometi 8718  blocnilem 8719  cnph 8734  ipasslem2 8747  ipasslem5 8750  ipdi 8759  ipsubdi 8765  ipblnfi 8772  ajmoi 8775  ubthlem3 8789  ubthlem5 8791  ubthlem6 8792  ubthlem7 8793  ubthlem10 8796  ubthlem11 8797  minveclem24 8828  minveclem25 8829  minveclem28 8832  htthlem8 8889  htthlem9 8890  sinper 8957  cosper 8958  abssinper 8980  efifolem7 9000  efif1lem5 9006  efper 9019  axgroth3 9051  hvsubopr 9160  hvsubcl 9162  hvaddsubval 9177  hvpncan 9183  hvaddeq0 9211  hvmulcan 9214  hvmulcanOLD 9215  his5 9229  his7 9232  his2sub2 9235  hlimcauii 9382  hhssnv 9410  shorth 9444  occllem6 9454  projlem25 9486  projlem26 9487  pjval 9515  pjeq2 9517  chsscon2 9701  chpsscon2 9704  chdmm3 9726  chdmm4 9727  chdmj3 9730  chdmj4 9731  chj4 9734  spansnmul 9763  cmcm2 9835  fh1 9837  fh2 9838  cm2j 9839  spansnscl 9871  spansncvi 9875  5oalem4 9880  homulcl 9965  homco1 10007  homulass 10008  hoadddi 10009  hosubneg 10013  honegsubdi 10016  hosubsub2 10018  hosub4 10019  adjmo 10038  adjsym 10039  cnvadj 10096  nmopub2tALT 10113  unoplin 10124  counop 10125  nmfnleub2 10130  hmoplin 10146  braadd 10149  bramul 10150  kbmul 10159  lnopmul 10170  lnopaddmuli 10176  lnopsubmuli 10178  homco2 10180  nmlnop0iALT 10199  lnopmi 10204  lnophsi 10205  lnopeq0i 10211  unopbd 10219  hmopd 10226  nmophmi 10240  lnopconi 10242  lnfnmuli 10252  lnfnaddmuli 10253  lnfnconi 10269  nlelshi 10272  riesz3i 10274  cnlnadjlem6 10284  adjlnop 10298  adjmul 10304  adjcoi 10312  cnvbramul 10328  leopnmid 10351  hmopidmpji 10360  pjadjcoi 10369  pjss1coi 10371  pjnormssi 10376  pjclem4 10408  pjadj2coi 10413  pj3si 10416  pj3i 10417  hstnmoc 10431  hstle1 10434  hst1h 10435  hstle 10438  hstoh 10440  spansncv2 10501  dmdmd 10508  mdslmd1lem2 10534  mdslmd2i 10538  atcveq0 10556  chcv1 10563  chcv2 10564  cvexchlem 10576  cvp 10583  atcv1 10589  atexch 10590  atomli 10591  atcvatlem 10594  irredlem2 10600  irredi 10603  atdmd 10607  atmd2 10609  mdsymlem3 10614  mdsymlem5 10616  atdmd2 10623  sumdmdlem 10627  sumdmdlem2 10628  cdj1i 10642  cdj3lem1 10643  cdj3lem2b 10646  cdj3i 10650  symggrpi 10691  cayleylem2 10695  11st22nd 10742  cbci 11003  subtopsin2 11067  cnfilca 11088  topunfincomp 11120  singcon 11137  iint 11157  issubcat 11299  finminlem 11418  elfiun 11421  ordtypelem5 11431  ordtypelem6 11432  omsubsdomlem2 11441  omsubel 11444  elomsubsd 11446  subntr 11482  cnsubsp2 11484  compsub 11488  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem3 11498  alexsub 11500  subtopmetlem 11505  reconnlem5 11511  reconn 11512  neibastop1 11579  topjoin 11588  fbssint 11626  fsubbas 11630  extbas1 11641  ufprim 11654  ufileu 11658  limfil 11675  flimopn 11679  neiplim 11681  limfilcf 11683  flimcls 11684  hausfillim 11685  cnpfillim 11686  filmapf 11688  isfilmap 11689  elfilmap 11690  elfilmap3 11692  fmf 11693  fmbas 11694  fmfnfmlem4 11703  fmfnfm 11704  isfclus 11718  fcluscomp 11733  sfclusf 11736  filnetlem3 11765  morex 11804  f1ocan1fv 11816  f1elima 11818  upixp 11823  indexf 11847  fipreima 11848  filbcmb 11857  fzm1 11867  sdclem1 11875  sdclem2 11876  sdc 11877  seqpo 11878  incsequz 11879  incsequz2 11880  fsum00 11883  fsumlt 11884  fsumlt1 11894  unopn 11898  subspopn 11900  subspabs 11903  neificl 11904  lpss2 11906  metsstop 11909  blhalf 11911  mettrifi 11912  mettrifi2 11913  geomcau 11914  lmclim2 11915  caushft 11916  iccdil 11926  lincmb01cmp 11942  lincmb01icc 11943  cnimass 11949  cnres 11950  cnresima 11952  cnss 11953  hmeocnv 11959  lmtlm 11969  uptx 11978  txcn 11979  txsubsp 11983  sstotbnd 11992  totbndss 11993  isbnd3 11997  totbndbnd 12000  ismtyhmeolem 12006  ismtyhmeo 12007  ismtyres 12010  heiborlem1 12011  heiborlem11 12021  heiborlem13 12023  heiborlem15 12025  heiborlem16 12026  heiborlem23 12033  heiborlem29 12039  heiborlem30 12040  heiborlem32 12042  heiborlem33 12043  heiborlem36 12046  heiborlem37 12047  heiborlem42 12052  rrndstprj2 12074  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  phtpycom 12092  phtpycolem1 12093  phtpycolem2 12094  phtpyco 12098

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