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 393  anidm 435  ancom 438  abai 482  anabs1 495  pm3.48 560  ibib 593  ordi 599  pm4.39 633  pm4.38 634  pm4.71 638  intnanr 696  intnanrd 698  biantrud 730  bianfd 742  pm5.75 753  dedlemb 767  nicodraw 956  19.26 1073  19.40 1100  sbequ2 1185  mopick2 1443  moexex 1445  2exeu 1453  2eu2 1457  r19.40 1769  reu3 1938  csbnestglem 2044  csbnest1g 2046  ssab2 2139  uneqin 2265  difprsn 2477  unissel 2539  ssmin 2564  iununi 2629  class2set 2747  moabex 2780  mosubopt 2818  ordsseleq 2990  onin 2992  ordsson 3005  opelxp 3228  ralxp 3232  xpss 3244  opabssxp 3248  dmcosseq 3379  relssres 3406  dminss 3476  cores 3513  fun11uni 3579  dffo4 3834  ffnfv 3842  isotr 3911  isotrALT 3912  isofrlem 3915  f1oiso 3918  tfrlem8 3932  tz7.48lem 3969  fnoprabg 4026  eloprabi 4132  omordi 4211  omord 4213  omlimcl 4223  oneo 4226  oen0 4227  oeordi 4228  oewordri 4233  oeordsuc 4235  eceqopreq 4327  th3qlem1 4328  fipr 4448  pw2en 4461  ssenen 4519  unblem2 4554  dfom3 4642  r1ord 4667  r1val1 4670  rankr1 4686  rankuni 4710  rankxplim3 4726  karden 4738  hta 4740  aceq3 4745  kmlem8 4784  kmlem16 4792  brdom7disj 4816  brdom6disj 4817  unidom 4820  cardalephex 4899  axunnd 4961  axacndlem1 4972  axacndlem3 4974  enqeceq 5060  distrpq 5080  genpnnp 5121  addclprlem2 5132  distrlem4pr 5143  prlem936 5168  reclem3pr 5171  suplem2pr 5175  enreceq 5190  mulcmpblnr 5196  pncan3t 5390  0re 5453  leltnet 5534  xrleltnet 5571  ltsubpost 5666  posdift 5667  subge0t 5687  recextlem1 5695  recid2t 5744  divcan5t 5785  divdivdivt 5789  divdivmult 5799  lemul12itOLD 5847  mulgt1t 5849  lt2mul2divt 5877  ltdiv2t 5893  ledivdivt 5896  lediv2t 5897  recp1lt1 5907  recrecltt 5908  ledivp1t 5911  1nn 5940  nnleltp1t 5960  avglet 6050  nnreclt 6078  flwordit 6246  flbi2t 6250  ceilet 6259  quoremz 6260  quoremnn0ALT 6261  quoremnn0 6262  intfracq 6264  qrecclt 6283  elioo3g 6329  elfz2t 6422  elfzlem 6423  elfz2nn0t 6445  fzaddelt 6450  fzrev2t 6462  fsequb 6473  seq1rn2 6504  ser1add2 6521  ser1add 6522  seqzp1 6561  seqzrn2 6569  expeq0t 6598  expgt0t 6602  expgt1t 6605  mulexpt 6607  recexpt 6608  subsqt 6655  bernneq 6665  creur 6756  replimt 6775  cjexpt 6831  absexpt 6882  absmaxt 6911  cvganz 6938  facavgt 6969  fsumsplit 7034  fsumadd 7036  fsumcom 7042  fsumrev 7043  fsumdivcALT 7050  fsumcmp0 7055  fsumcmpndx2 7056  serzmulc1 7071  bcxmas 7090  clm3 7093  clm4le 7095  climge0 7126  climaddlem3 7130  climaddc1 7132  climmullem8 7141  climmulc2 7143  climsubc2 7145  iserzmulc1 7150  climcmpc1 7153  climsqueeze 7154  climsqueeze2 7155  caucvglem2 7172  caucvglem4 7174  caucvglem5 7175  caucvglem6 7176  iserzgt0 7225  infcvglem3 7237  georeclim 7254  geoisumr 7257  geoisum1c 7259  cvgratlem1 7264  cncfval 7278  ivthlem7 7301  efaddlem10 7361  efaddlem23 7374  efaddlem25 7376  efexpt 7386  acdc2lem2 7504  acdc5lem2 7507  infmap2lem1 7594  infmap2lem2 7595  gch-kn 7602  basgen2t 7651  indistop 7658  indistopOLD 7659  cctop 7661  clscld 7692  elcls 7713  ntrcls0 7716  neii1 7730  neissex 7747  islp2 7756  ismsg 7809  meteq0 7821  blin 7861  blss 7862  opnfss 7867  lpbl 7889  metcnplem 7895  metcnpi3 7901  metcnpi4 7902  metcni2 7904  tgioolem 7923  dscmet 7927  lmbr 7937  lmnn 7944  lmuni 7960  lmsslem 7961  metelcls 7974  bcthlem8 8015  bcthlem10 8017  bcthlem17 8024  bcthlem26 8033  isgrp 8050  grpidinvlem2 8058  grpidinv 8061  grpinveu 8072  grpinv 8077  grpdivdiv 8095  grpmuldivass 8096  grppnpcan2 8100  abldivdiv4 8117  ringsn 8171  vcid 8178  vcdi 8179  vcdir 8180  nvzs 8273  nvmf 8274  nvmdi 8278  nvmtri2 8308  imsmetlem 8331  nmoub3i 8444  nmlno0lem 8461  nmblolbii 8467  ipdi 8511  ipassr 8514  ipsubdi 8517  ip2eqi 8525  ubthlem8 8544  ubthlem9 8545  ubthlem10 8546  ubthlem11 8547  pstr 8660  efif1lem3 8739  shftefif1olem 8748  hvaddsub4t 8952  norm1t 9128  norm1ex 9129  hhsscms 9157  chocuni 9179  occllem6 9185  projlem26 9218  pjtheu 9242  chabs1t 9446  normcant 9506  pjspansnt 9507  h1datom 9511  pjoml5t 9563  osumlem7 9591  5oalem1 9606  5oalem2 9607  5oalem5 9610  3oalem2 9615  pjidt 9647  pjds3 9665  nmopub2tALT 9840  cnvunopt 9849  unoplint 9851  counopt 9852  nmfnleub2t 9857  hmoplint 9873  nmlnop0ALT 9927  nmbdoplb 9956  nmcopexlem5 9962  nmcoplb 9965  nmbdfnlb 9985  nmcfnexlem5 9991  nmcfnlb 9994  riesz3 10002  riesz4 10003  cnlnadjeu 10017  adjlnopt 10026  branmfnt 10045  kbass5t 10060  leopsqt 10069  nmopleidt 10079  hmopidmpj 10087  pjclem4 10135  pj3s 10143  stge0t 10159  cvpsst 10220  ssmd2 10247  mdslj1 10254  mdslj2 10255  mdslmd1lem1 10260  mdslmd1lem2 10261  atcvat3 10331  atcvat4 10332  mdsymlem2 10339  mdsymlem3 10340  mdsymlem5 10342  cdj1 10368  hmphre 10536  hmeogrp 10544  fgsb 10575  fgsb2 10580  rcfpfillem3 10585  trnij 10628  homib 10715  icmpmon 10735  immon 10737  idfisf 10752

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