Theorem pm3.26 319

Description: Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112.

Assertion

Ref	Expression
pm3.26	|- ((ph /\ ps) -> ph)

Proof of Theorem pm3.26

Step	Hyp	Ref	Expression
1		df-an 225	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2		pm3.26im 139	. 2 |- (-. (ph -> -. ps) -> ph)
3	1, 2	sylbi 199	1 |- ((ph /\ ps) -> ph)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223

This theorem is referenced by:  pm3.26i 320  pm3.26d 321  pm3.41 327  ancrb 330  pm4.45im 332  anim12i 333  pm4.44 345  adantrd 391  anidm 432  ancom 435  abai 478  anabs1 491  pm3.48 555  ibib 588  ordi 594  pm4.39 628  pm4.38 629  pm4.71 633  intnanr 689  intnanrd 691  biantrud 723  bianfd 735  pm5.75 746  dedlemb 760  nicodraw 948  19.26 1043  19.40 1070  sbequ2 1162  mopick2 1413  moexex 1415  2exeu 1423  2eu2 1427  r19.40 1738  reu3 1902  csbnestglem 2006  csbnest1g 2008  ssab2 2101  uneqin 2227  difprsn 2435  unissel 2495  ssmin 2520  iununi 2584  class2set 2702  moabex 2734  mosubopt 2767  ordsseleq 2939  onin 2941  ordsson 2954  ralxp 3180  xpss 3192  opabssxp 3196  dmcosseq 3316  relssres 3343  dminss 3411  cores 3441  fun11uni 3505  dffo4 3759  ffnfv 3767  isotr 3836  isotrALT 3837  isofrlem 3840  f1oiso 3843  tfrlem8 3857  tz7.48lem 3894  fnoprabg 3951  eloprabi 4056  omordi 4135  omord 4137  omlimcl 4147  oneo 4150  oen0 4151  oeordi 4152  oewordri 4157  oeordsuc 4159  eceqopreq 4251  th3qlem1 4252  pw2en 4380  ssenen 4436  unblem2 4470  dfom3 4554  r1ord 4579  r1val1 4582  rankr1 4598  rankuni 4622  rankxplim3 4638  karden 4650  hta 4652  aceq3 4657  kmlem8 4696  kmlem16 4704  brdom7disj 4728  brdom6disj 4729  unidom 4732  cardalephex 4809  axunnd 4871  axacndlem1 4882  axacndlem3 4884  enqeceq 4970  distrpq 4990  genpnnp 5031  addclprlem2 5042  distrlem4pr 5053  prlem936 5078  reclem3pr 5081  suplem2pr 5085  enreceq 5100  mulcmpblnr 5106  pncan3t 5300  0re 5363  leltnet 5445  xrleltnet 5482  ltsubpost 5577  posdift 5578  subge0t 5598  recextlem1 5606  recid2t 5650  divcan5t 5688  divdivdivt 5692  divdivmult 5702  ltmul12it 5748  lemul12itOLD 5750  mulgt1t 5752  lt2mul2divt 5773  ltdiv2t 5786  ledivdivt 5789  lediv2t 5790  recp1lt1 5800  recrecltt 5801  ledivp1t 5804  1nn 5833  nnleltp1t 5852  avglet 5942  nnreclt 5970  flwordit 6134  ceilet 6144  qrecclt 6162  seq1rn2 6209  ser1add2 6226  ser1add 6227  elioo3g 6268  elfz2t 6355  elfzlem 6356  elfz2nn0t 6378  fzaddelt 6383  fzrev2t 6395  fsequb 6406  seqzp1 6431  seqzrn2 6439  expeq0t 6468  expgt0t 6471  expgt1t 6474  mulexpt 6476  recexpt 6477  subsqt 6524  bernneq 6534  creur 6624  replimt 6643  cjexpt 6703  absexpt 6754  cvganz 6812  facavgt 6843  fsumsplit 6909  fsumadd 6911  fsumcom 6917  fsumrev 6918  fsumdivcALT 6925  fsumcmp0 6930  fsumcmpndx2 6931  serzmulc1 6946  bcxmas 6965  clm3 6968  clm4le 6970  climge0 7000  climaddlem3 7003  climaddc1 7005  climmullem8 7014  climmulc2 7016  climsubc2 7018  iserzmulc1 7023  climcmpc1 7026  climsqueeze 7027  climsqueeze2 7028  caucvglem2 7045  caucvglem4 7047  caucvglem5 7048  caucvglem6 7049  iserzgt0 7097  infcvglem3 7109  georeclim 7126  geoisumr 7129  geoisum1c 7131  cvgratlem1 7136  cncfval 7150  ivthlem7 7173  ivthlem7OLD 7182  efaddlem10 7240  efaddlem23 7253  efaddlem25 7255  efexpt 7265  acdc2lem2 7382  acdc5lem2 7385  infmap2lem1 7472  infmap2lem2 7473  gch-kn 7480  basgen2t 7532  indistop 7541  fctop 7543  cctop 7545  clscld 7576  elcls 7596  neii1 7610  neissex 7627  islp2 7636  ismsg 7687  meteq0 7699  blin 7740  blss 7741  opnfss 7746  lpbl 7767  metcnplem 7773  metcnpi3 7779  metcnpi4 7780  metcni2 7782  tgioolem 7801  dscmet 7804  lmbr 7814  lmnn 7821  lmuni 7834  lmsslem 7835  metelcls 7848  bcthlem8 7888  bcthlem10 7890  bcthlem17 7897  bcthlem26 7906  isgrp 7923  grpidinvlem2 7931  grpidinv 7934  grpinveu 7946  grpinv 7951  grpdivdiv 7970  grpmuldivass 7971  grppnpcan2 7975  abldivdiv4 7994  ringsn 8048  vcid 8057  vcdi 8058  vcdir 8059  nvzs 8142  nvmf 8143  nvmdi 8147  nvmtri2 8176  imsmetlem 8198  nmoub3i 8303  nmlno0lem 8320  nmblolbii 8325  ipdi 8369  ipassr 8372  ipsubdi 8375  ip2eqi 8383  ubthlem8 8402  ubthlem9 8403  ubthlem10 8404  ubthlem11 8405  efif1lem3 8560  shftefif1olem 8574  shftefif1olemOLD 8575  hmphre 8768  hmeogrp 8776  fgsb 8794  fgsb2 8799  trnij 8831  homib 8918  icmpmon 8937  hvaddsub4t 9094  norm1t 9272  norm1ex 9273  chocuni 9302  occllem6 9308  projlem26 9341  pjtheu 9364  chabs1t 9568  normcant 9630  pjspansnt 9631  h1datom 9635  pjoml5t 9687  osumlem7 9715  5oalem1 9730  5oalem2 9731  5oalem5 9734  3oalem2 9739  pjidt 9771  pjds3 9789  nmopub2tALT 9964  cnvunopt 9972  unoplint 9974  counopt 9975  nmfnleub2t 9980  hmoplint 9996  nmlnop0ALT 10049  nmbdoplb 10078  nmcopexlem5 10084  nmcoplb 10087  nmbdfnlb 10107  nmcfnexlem5 10113  nmcfnlb 10116  riesz3 10124  riesz4 10125  cnlnadjeu 10139  adjlnopt 10148  branmfnt 10165  kbass5t 10179  leopsqt 10188  nmopleidt 10197  hmopidmpj 10205  pjclem4 10251  pj3s 10259  stge0t 10275  cvpsst 10336  ssmd2 10361  mdslj1 10368  mdslj2 10369  mdslmd1lem1 10374  mdslmd1lem2 10375  atcvat3 10445  atcvat4 10446  mdsymlem2 10453  mdsymlem3 10454  mdsymlem5 10456  cdj1 10479

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