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 1368  ax11inda2ALT 1369  elabgt 1895  sbciegft 1959  hbsbc1gd 1983  hbsbcgd 1984  hbcsb1gd 2027  hbcsbgd 2028  csbnestg 2036  sbcnestg 2038  sspr 2475  ssiun 2592  uniexb 2907  trssord 2965  ordelssne 2974  onint 3006  onint0 3007  onnmin 3015  onsssuc 3058  onsucmin 3072  ordsucun 3082  nlimsucg 3112  ordunisuc2 3115  peano5 3153  findsg 3157  tfindsg 3162  tfindsg2 3163  cnvexg 3519  coexg 3524  funimass2 3573  cofunexg 3580  cofunex2g 3581  dmfex 3655  funbrfv 3750  eqfnfv 3797  fvimacnvi 3804  fvimacnvALT 3809  funiunfv 3866  isofrlem 3901  tfrlem8 3918  tfrlem9 3919  tfrlem11 3921  tfr3 3926  foprrn 4035  fnoprvalrn 4038  oasuc 4163  omsuc 4165  oalim 4167  omlim 4168  oalimcl 4194  oaass 4195  omlimcl 4209  odi 4210  omass 4211  oneo 4212  oelim2 4222  nnaordex 4249  nnawordex 4250  oaabslem 4251  ecoprass 4320  ecoprdi 4321  mapex 4328  f1oen2g 4394  f1oeng 4395  domentr 4421  undom 4438  pwuninel 4486  mapunen 4502  ssenen 4504  phplem3 4510  phplem4 4511  php 4513  php3 4515  php3OLD 4516  onomeneq 4519  omsucdom 4523  ssfi 4537  ssfiOLD 4538  unbnn2 4545  unfi 4551  unfiOLD 4552  unifiOLD 4557  fodomfiOLD 4566  iunfiOLD 4569  pm54.43 4572  supmaxlem 4588  omex 4627  aceq3 4733  aceq5 4740  aceq6b 4742  ac5b 4753  zorn2lem3 4790  imadomg 4806  sucdom 4842  ondomon 4856  alephnbtwn 4868  alephordi 4874  alephval2 4902  cfom 4916  axrepndlem2 4945  axpowndlem4 4952  axinfndlem1 4957  axacndlem5 4963  addclpi 5020  addasspi 5023  mulasspi 5025  distrpi 5026  mulcanpi 5027  indpi 5034  ltapq 5076  ltrpq 5085  prcdpq 5097  genpass 5112  distrlem1pr 5127  distrlem2pr 5128  distrlem4pr 5130  psslinpr 5135  prlem934b 5138  ltexprlem6 5147  ltexprlem7 5148  prlem936b 5154  prlem936 5155  reclem3pr 5158  reclem4pr 5159  recexsrlem 5212  suppsr3 5224  pre-axsup 5291  cnegextlem1 5345  cnegextlem3 5347  cnegext 5348  subnegt 5394  subdit 5427  1re 5435  resubclt 5438  mulneg2t 5452  negsubdit 5457  submul2t 5460  subsub2t 5461  nnncan1t 5467  addsub4t 5473  xrret 5569  le2tri3 5589  ltaddsubt 5631  leaddsubt 5633  lenegcon2t 5659  recextlem1 5682  recextlem2 5683  recext 5684  divnegt 5774  letrp1t 5816  lerec2t 5889  ledivdivt 5890  lediv12it 5896  ledivp1t 5905  nndivt 5959  nndivtrt 5960  lble 6047  sup2 6051  dfinfmr 6067  nnunb 6070  arch 6071  bndndx 6073  xrsupsslem 6076  xrinfmsslem 6077  supxrunb1 6089  nn0ge0t 6117  nn0addclt 6120  nn0leltp1t 6128  nn0addge1t 6130  nn0addge2t 6131  zaddclt 6165  zsubclt 6168  zrevaddclt 6170  elnn0nn 6171  zltp1let 6181  zleltp1t 6182  zltlem1t 6184  peano2uz2 6201  uzind 6205  uzindOLD 6208  uzwo4OLD 6210  uzwo3lem1 6216  zmax 6220  zbtwnre 6221  rebtwnz 6222  flget 6233  flwordit 6237  flbit 6240  fladdzt 6244  qaddclt 6269  qsubclt 6272  qrecclt 6273  qdivclt 6274  qrevaddclt 6275  qbtwnre 6278  qsqueeze 6280  seq1rn2 6321  ser1recl 6331  elioc2t 6390  elico2t 6391  elicc2t 6392  icounlem 6412  eluzp1lt 6434  uzwo 6455  uzwoOLD 6456  fzss2t 6504  fzrev2t 6512  fzrev3it 6515  fzrevralt 6519  fsequb 6523  fsequb2 6524  fseqsupub 6526  seqzp1 6548  seqzval2t 6553  seqzeq 6555  seqzrn2 6556  seqzrn 6557  ser0cl1 6564  expnnvalt 6572  expp1t 6574  expm1t 6583  expeq0t 6585  expge0t 6591  expgt1t 6592  expge1t 6593  bernneq 6652  expnlbndt 6655  replimt 6761  mulretOLD 6777  resubt 6806  imsubt 6809  cjsubt 6816  sqabsaddt 6848  sqabssubt 6849  seq1bnd 6910  cau3ir 6915  cau5i 6917  cvg2 6922  facclt 6940  facdivt 6942  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd5 6953  bccmplt 6962  fsum1s 7009  fsump1s 7013  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsumshft 7031  fsummulc1 7033  fsummulc2 7034  fsum2mul 7037  fsumconst 7038  fsumcmp 7040  fsumcmp0 7041  fsumcmpndx2 7042  fsumabs 7043  fsumabs2mul 7044  serzcl2t 7049  serzcmp0 7055  binomlem1 7066  binomlem2 7067  binomlem5 7070  binomlem6 7071  clm4 7080  clm4le 7081  clm4f 7082  clm4at 7090  climfnn 7092  2climnn 7102  2climnn0 7103  iserzshft2 7107  climge0 7112  climaddlem3 7116  climaddc1 7118  climmullem3 7122  climmullem5 7124  climmullem8 7127  climmulc2 7129  climsubc2 7131  clim2serzt 7134  iserzmulc1 7136  iserzcmp 7142  clim2serz 7145  climserzle 7147  climsup 7155  caucvglem6 7162  isumreclt 7210  expcnv 7233  geoisum1c 7245  cvgratlem1ALT 7247  cvgratlem2ALT 7248  cvgratlem1 7250  cvgratlem2 7251  cvgratlem4 7253  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag 7258  fsum0diag2 7259  mulc1cncf 7279  ivthlem7 7287  efcltlem1 7304  erelem1 7319  erelem3 7321  efaddlem5 7342  efaddlem6 7343  efsubt 7371  efexpt 7372  reeftlclt 7380  sinsubt 7455  cossubt 7456  demoivreALT 7485  acdc5lem1 7491  acdcALT 7496  znnenlem 7501  unbenlem 7504  ruclem13 7522  infxpidmlem1 7552  infxpidmlem8 7559  infxpidmlem11 7562  infxpidmlem12 7563  infdif 7568  iunopnt 7599  istps3 7608  eltgt 7618  eltg2t 7619  tgclt 7624  tgval3t 7625  basgen2t 7639  bastop 7642  subbas2OLD 7645  fctopOLD 7650  clsval2 7685  ntrss 7688  isnei 7718  isneip 7720  neips 7727  islp2 7747  iscncl 7770  metreslem 7822  blin 7852  blss 7853  isopn4 7862  opnin 7869  metcnpi3 7892  metcnpi4 7893  metcni2 7895  metcnss 7898  metcnss2 7899  lmbr 7928  lmnn 7935  lmuni 7951  causs 7955  lmfexlem2 7957  metelcls 7965  metcnp4 7970  xplmi2 7974  opr1cn 7978  lmcau 7996  bcthlem1 7999  bcthlem9 8007  bcthlem10 8008  bcthlem14 8012  bcthlem16 8014  bcthlem21 8019  grpidinvlem1 8048  grpidinvlem2 8049  grpideu 8053  resgrprn 8095  grplactfval 8096  ablnncan 8112  issubgi 8122  ablmul 8131  ghgrpilem4 8136  isvc 8200  isnv 8231  nvmul0or 8272  imsmetlem 8323  nvcni3 8331  nvlmle 8333  nmcnilem 8337  sm1cnilem 8347  ipcl 8365  ip1cnilem2 8374  ip1cnilem3 8375  ip1cnilem5 8377  ip1cnilem6 8378  sspival 8397  lnocoi 8418  nmosetre 8427  nmoge0 8430  nmoub3i 8436  nmobndi 8438  nmlno0lem 8453  blo3i 8462  blometi 8463  blocnilem 8464  cnph 8478  ipasslem2 8491  ipasslem5 8494  ipdi 8503  ipsubdi 8509  ipblnfi 8516  ajmoi 8519  ubthlem3 8531  ubthlem5 8533  ubthlem6 8534  ubthlem7 8535  ubthlem10 8538  ubthlem11 8539  minveclem24 8568  minveclem25 8569  minveclem28 8572  htthlem8 8627  htthlem9 8628  sinper 8690  cosper 8691  abssinper 8712  efifolem7 8728  efif1lem5 8734  efper 8747  axgroth3 8779  hvsubopr 8885  hvsubclt 8887  hvaddsubvalt 8902  hvpncant 8908  hvaddeq0t 8936  hvmulcant 8939  his5t 8953  his7t 8956  his2sub2t 8959  hlimcaui 9106  hhssnv 9134  shorth 9168  occllem6 9178  projlem25 9210  projlem26 9211  pjvalt 9239  pjeq2t 9241  chsscon2t 9425  chpsscon2t 9428  chdmm3t 9450  chdmm4t 9451  chdmj3t 9454  chdmj4t 9455  chj4t 9458  spansnmul 9487  cmcm2t 9559  fh1t 9561  fh2t 9562  cm2jt 9563  spansnsclt 9593  spansncv 9597  5oalem4 9602  homulclt 9685  homco1t 9727  homulasst 9728  hoadddit 9729  hosubnegt 9733  honegsubdit 9736  hosubsub2t 9738  hosub4t 9739  adjmo 9758  adjsymt 9759  cnvadj 9816  nmopub2tALT 9833  unoplint 9844  counopt 9845  nmfnleub2t 9850  hmoplint 9866  braaddt 9869  bramult 9870  kbmult 9879  lnopmult 9891  lnopaddmul 9897  lnopsubmul 9899  homco2t 9901  nmlnop0ALT 9920  lnopm 9925  lnophs 9926  lnopeq0 9932  unopbdt 9940  hmopdt 9947  nmophm 9961  lnopcon 9963  lnfnmul 9973  lnfnaddmul 9974  lnfncon 9990  nlelsh 9993  riesz3 9995  cnlnadjlem6 10005  adjlnopt 10019  adjmult 10025  adjco 10033  cnvbramult 10048  leopnmidt 10071  hmopidmpj 10080  pjadjco 10089  pjss1co 10091  pjnormss 10096  pjclem4 10127  pjadj2co 10132  pj3s 10135  pj3 10136  hstnmoct 10150  hstle1t 10153  hst1ht 10154  hstlet 10157  hstoht 10159  spansncv2t 10220  dmdmdt 10227  mdslmd1lem2 10253  mdslmd2 10257  atcveq0 10275  chcv1t 10282  chcv2t 10283  cvexchlem 10295  cvp 10302  atcv1t 10307  atexcht 10308  atoml 10309  atcvatlem 10312  irredlem2 10318  irred 10321  atdmd 10325  atmd2 10327  mdsymlem3 10332  mdsymlem5 10334  atdmd2 10341  sumdmdlem 10345  sumdmdlem2 10346  cdj1 10360  cdj3lem1 10361  cdj3lem2b 10364  cdj3 10368  symggrpi 10406  cayleylem2 10410  11st22nd 10458  cnfilca 10583  cnfilcaOLD 10584  iint 10634

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