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 1345  ax11inda2ALT 1346  elabgt 1867  sbciegft 1930  hbsbc1gd 1954  hbsbcgd 1955  hbcsb1gd 1998  hbcsbgd 1999  csbnestg 2007  sbcnestg 2009  sspr 2445  ssiun 2560  uniexb 2870  trssord 2928  ordelssne 2937  onint 2969  onint0 2970  onnmin 2978  onsssuc 3021  onsucmin 3035  ordsucun 3045  nlimsucg 3075  ordunisuc2 3078  peano5 3116  findsg 3120  tfindsg 3125  tfindsg2 3126  cnvexg 3460  coexg 3465  funimass2 3513  cofunexg 3520  cofunex2g 3521  dmfex 3594  funbrfv 3689  eqfnfv 3736  fvimacnvi 3743  fvimacnvALT 3748  funiunfv 3805  isofrlem 3840  tfrlem8 3857  tfrlem9 3858  tfrlem11 3860  tfr3 3865  foprrn 3974  fnoprvalrn 3977  oasuc 4101  omsuc 4103  oalim 4105  omlim 4106  oalimcl 4132  oaass 4133  omlimcl 4147  odi 4148  omass 4149  oneo 4150  oelim2 4160  nnaordex 4187  nnawordex 4188  oaabslem 4189  ecoprass 4258  ecoprdi 4259  mapex 4266  f1oen2g 4329  f1oeng 4330  domentr 4356  undom 4372  mapunen 4434  ssenen 4436  phplem3 4442  phplem4 4443  php 4445  php3 4447  onomeneq 4450  omsucdom 4454  ssfi 4467  unbnn2 4474  unfi 4480  unifi 4484  fodomfi 4492  iunfi 4495  pm54.43 4498  omex 4551  aceq3 4657  aceq5 4664  aceq6b 4666  ac5b 4677  zorn2lem3 4714  imadomg 4730  sucdom 4765  ondomon 4779  alephnbtwn 4791  alephordi 4797  alephval2 4825  cfom 4839  axrepndlem2 4868  axpowndlem4 4875  axinfndlem1 4880  axacndlem5 4886  addclpi 4943  addasspi 4946  mulasspi 4948  distrpi 4949  mulcanpi 4950  indpi 4957  ltapq 4999  ltrpq 5008  prcdpq 5020  genpass 5035  distrlem1pr 5050  distrlem2pr 5051  distrlem4pr 5053  psslinpr 5058  prlem934b 5061  ltexprlem6 5070  ltexprlem7 5071  prlem936b 5077  prlem936 5078  reclem3pr 5081  reclem4pr 5082  recexsrlem 5135  suppsr3 5147  pre-axsup 5214  cnegextlem1 5268  cnegextlem3 5270  cnegext 5271  subnegt 5317  subdit 5350  1re 5358  resubclt 5361  mulneg2t 5375  negsubdit 5380  submul2t 5383  subsub2t 5384  nnncan1t 5390  addsub4t 5396  xrret 5493  le2tri3 5514  ltaddsubt 5556  leaddsubt 5558  lenegcon2t 5583  recextlem1 5606  recextlem2 5607  recext 5608  divnegt 5681  letrp1t 5723  lerec2t 5788  ledivdivt 5789  lediv12it 5795  ledivp1t 5804  nndivt 5857  nndivtrt 5858  lble 5945  sup2 5949  dfinfmr 5965  nnunb 5968  arch 5969  bndndx 5971  xrsupsslem 5974  xrinfmsslem 5975  supxrunb1 5987  nn0ge0t 6015  nn0addclt 6018  nn0leltp1t 6026  nn0addge1t 6028  nn0addge2t 6029  zaddclt 6063  zsubclt 6066  zrevaddclt 6068  elnn0nn 6069  zltp1let 6079  zleltp1t 6080  zltlem1t 6082  peano2uz2 6100  uzind 6104  uzindOLD 6107  uzwo4OLD 6109  uzwo3lem1 6115  zmax 6119  zbtwnre 6120  rebtwnz 6121  flget 6129  flwordit 6134  flbit 6135  fladdzt 6138  qaddclt 6158  qsubclt 6161  qrecclt 6162  qdivclt 6163  qrevaddclt 6164  qbtwnre 6167  qsqueeze 6169  seq1rn2 6209  ser1recl 6219  elioc2t 6273  elico2t 6274  elicc2t 6275  icounlem 6296  eluzp1lt 6317  uzwo 6338  uzwoOLD 6339  fzss2t 6387  fzrev2t 6395  fzrev3it 6398  fzrevralt 6402  fsequb 6406  fsequb2 6407  fseqsupub 6409  seqzp1 6431  seqzval2t 6436  seqzeq 6438  seqzrn2 6439  seqzrn 6440  ser0cl1 6447  expnnvalt 6455  expp1t 6457  expm1t 6466  expeq0t 6468  expge0t 6473  expgt1t 6474  expge1t 6475  bernneq 6534  replimt 6643  resubt 6692  imsubt 6695  cjsubt 6702  sqabsaddt 6734  sqabssubt 6735  seq1bnd 6798  cau3ir 6803  cau5i 6805  cvg2 6810  facclt 6828  facdivt 6830  faclbnd4lem3 6838  faclbnd4lem4 6839  faclbnd5 6841  bccmplt 6851  fsum1s 6898  fsump1s 6902  fsum1ps 6907  fsumsplit 6909  fsumadd 6911  fsumcom 6917  fsumrev 6918  fsumshft 6920  fsummulc1 6922  fsummulc2 6923  fsum2mul 6926  fsumconst 6927  fsumcmp 6929  fsumcmp0 6930  fsumcmpndx2 6931  fsumabs 6932  fsumabs2mul 6933  serzcl2t 6938  serzcmp0 6944  binomlem1 6955  binomlem2 6956  binomlem5 6959  binomlem6 6960  clm4 6969  clm4le 6970  clm4f 6971  clm4at 6979  climfnn 6981  2climnn 6990  2climnn0 6991  iserzshft2 6995  climge0 7000  climaddlem3 7003  climaddc1 7005  climmullem3 7009  climmullem5 7011  climmullem8 7014  climmulc2 7016  climsubc2 7018  clim2serzt 7021  iserzmulc1 7023  iserzcmp 7029  clim2serz 7032  climserzle 7034  climsup 7042  caucvglem6 7049  isumreclt 7096  expcnv 7119  geoisum1c 7131  cvgratlem1ALT 7133  cvgratlem2ALT 7134  cvgratlem1 7136  cvgratlem2 7137  cvgratlem4 7139  cvgratlem5 7140  fsum0diaglem2 7143  fsum0diag 7144  fsum0diag2 7145  mulc1cncf 7165  ivthlem7 7173  ivthlem7OLD 7182  efcltlem1 7197  erelem1 7212  erelem3 7214  efaddlem5 7235  efaddlem6 7236  efsubt 7264  efexpt 7265  reeftlclt 7273  sinsubt 7348  cossubt 7349  demoivreALT 7378  acdc5lem1 7384  acdcALT 7389  znnenlem 7394  znnenlemOLD 7395  unbenlem 7398  ruclem13 7416  infxpidmlem1 7446  infxpidmlem8 7453  infxpidmlem11 7456  infxpidmlem12 7457  infdif 7462  iunopnt 7492  istps3 7501  eltgt 7511  eltg2t 7512  tgclt 7517  tgval3t 7518  basgen2t 7532  bastop 7535  subbas2 7538  fctop 7543  clsval2 7578  ntrss 7581  isnei 7607  isneip 7609  neips 7616  islp2 7636  iscncl 7657  metreslem 7710  blin 7740  blss 7741  isopn4 7750  opnin 7757  metcnpi3 7779  metcnpi4 7780  metcni2 7782  metcnss 7785  metcnss2 7786  lmbr 7814  lmnn 7821  lmuni 7834  causs 7838  lmfexlem2 7840  metelcls 7848  metcnp4 7852  xplmi2 7856  opr1cn 7860  lmcau 7878  bcthlem1 7881  bcthlem9 7889  bcthlem10 7890  bcthlem14 7894  bcthlem16 7896  bcthlem21 7901  grpidinvlem1 7930  grpidinvlem2 7931  grpideu 7935  resgrprn 7978  grplactfval 7980  ablnncan 7997  issubgi 8007  ablmul 8016  ghgrpilem4 8021  nvmul0or 8149  imsmetlem 8198  nvlmle 8205  nmcnilem 8209  sm1cnilem 8216  ipcl 8234  ip1cnilem2 8243  ip1cnilem3 8244  ip1cnilem5 8246  ip1cnilem6 8247  sspival 8266  lnocoi 8287  nmosetre 8294  nmoge0 8297  nmoub3i 8303  nmobndi 8305  nmlno0lem 8320  blo3i 8328  blometi 8329  blocnilem 8330  cnph 8344  ipasslem2 8357  ipasslem5 8360  ipdi 8369  ipsubdi 8375  ipblnfi 8382  ajmoi 8385  ubthlem3 8397  ubthlem5 8399  ubthlem6 8400  ubthlem7 8401  ubthlem10 8404  ubthlem11 8405  minveclem24 8434  minveclem25 8435  minveclem28 8438  htthlem8 8491  htthlem9 8492  sinper 8522  cosper 8523  efifolem7 8556  efif1lem5 8562  circgrpOLD 8571  efper 8582  axgroth3 8631  symggrpi 8673  cayleylem2 8677  11st22nd 8713  cnfilca 8801  iint 8828  hvsubopr 9034  hvsubclt 9036  hvaddsubvalt 9051  hvpncant 9057  hvaddeq0t 9085  hvmulcant 9088  his5t 9102  his7t 9105  his2sub2t 9108  hlimcaui 9257  shorth 9298  occllem6 9308  projlem25 9340  projlem26 9341  pjvalt 9368  pjeq2t 9370  chsscon2t 9554  chpsscon2t 9557  chdmm3t 9579  chdmm4t 9580  chdmj3t 9583  chdmj4t 9584  chj4t 9587  spansnmul 9617  cmcm2t 9690  fh1t 9692  fh2t 9693  cm2jt 9694  spansnsclt 9724  spansncv 9728  5oalem4 9733  homulclt 9816  homco1t 9858  homulasst 9859  hoadddit 9860  hosubnegt 9864  honegsubdit 9867  hosubsub2t 9869  hosub4t 9870  adjmo 9889  adjsymt 9890  cnvadj 9947  nmopub2tALT 9964  unoplint 9974  counopt 9975  nmfnleub2t 9980  hmoplint 9996  braaddt 9999  bramult 10000  kbmult 10009  lnopmult 10021  lnopaddmul 10027  lnopsubmul 10029  homco2t 10031  nmlnop0ALT 10049  lnopm 10054  lnophs 10055  lnopeq0 10061  unopbdt 10069  hmopdt 10076  nmophm 10090  lnopcon 10092  lnfnmul 10102  lnfnaddmul 10103  lnfncon 10119  nlelsh 10122  riesz3 10124  cnlnadjlem6 10134  adjlnopt 10148  adjmult 10153  adjco 10161  cnvbramult 10174  leopnmidt 10196  hmopidmpj 10205  pjadjco 10214  pjss1co 10216  pjnormss 10221  pjclem4 10251  pjadj2co 10256  pj3s 10259  pj3 10260  hstnmoct 10274  hstle1t 10277  hst1ht 10278  hstlet 10281  hstoht 10283  spansncv2t 10344  dmdmdt 10351  mdslmd1lem2 10375  mdslmd2 10379  atcveq0 10397  chcv1t 10404  chcv2t 10405  cvexchlem 10417  cvp 10424  atcv1t 10429  atexcht 10430  atoml 10431  atcvatlem 10434  irredlem2 10440  irred 10443  atdmd 10447  atmd2 10449  mdsymlem3 10454  mdsymlem5 10456  sumdmdlem 10466  sumdmdlem2 10467  cdj1 10479  cdj3lem1 10480  cdj3lem2b 10483  cdj3 10487

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