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 479  anabs1 492  pm3.48 557  ibib 590  ordi 596  pm4.39 630  pm4.38 631  pm4.71 635  intnanr 692  intnanrd 694  biantrud 726  bianfd 738  pm5.75 749  dedlemb 763  nicodraw 952  19.26 1067  19.40 1094  sbequ2 1179  mopick2 1436  moexex 1438  2exeu 1446  2eu2 1450  r19.40 1762  reu3 1931  csbnestglem 2035  csbnest1g 2037  ssab2 2130  uneqin 2256  difprsn 2465  unissel 2527  ssmin 2552  iununi 2616  class2set 2734  moabex 2766  mosubopt 2804  ordsseleq 2976  onin 2978  ordsson 2991  opelxp 3214  ralxp 3218  xpss 3230  opabssxp 3234  dmcosseq 3365  relssres 3392  dminss 3462  cores 3499  fun11uni 3565  dffo4 3820  ffnfv 3828  isotr 3897  isotrALT 3898  isofrlem 3901  f1oiso 3904  tfrlem8 3918  tz7.48lem 3955  fnoprabg 4012  eloprabi 4118  omordi 4197  omord 4199  omlimcl 4209  oneo 4212  oen0 4213  oeordi 4214  oewordri 4219  oeordsuc 4221  eceqopreq 4313  th3qlem1 4314  pw2en 4446  ssenen 4504  unblem2 4541  dfom3 4630  r1ord 4655  r1val1 4658  rankr1 4674  rankuni 4698  rankxplim3 4714  karden 4726  hta 4728  aceq3 4733  kmlem8 4772  kmlem16 4780  brdom7disj 4804  brdom6disj 4805  unidom 4808  cardalephex 4886  axunnd 4948  axacndlem1 4959  axacndlem3 4961  enqeceq 5047  distrpq 5067  genpnnp 5108  addclprlem2 5119  distrlem4pr 5130  prlem936 5155  reclem3pr 5158  suplem2pr 5162  enreceq 5177  mulcmpblnr 5183  pncan3t 5377  0re 5440  leltnet 5521  xrleltnet 5558  ltsubpost 5653  posdift 5654  subge0t 5674  recextlem1 5682  recid2t 5736  divcan5t 5781  divdivdivt 5785  divdivmult 5795  lemul12itOLD 5843  mulgt1t 5845  lt2mul2divt 5872  ltdiv2t 5887  ledivdivt 5890  lediv2t 5891  recp1lt1 5901  recrecltt 5902  ledivp1t 5905  1nn 5934  nnleltp1t 5954  avglet 6044  nnreclt 6072  flwordit 6237  flbi2t 6241  ceilet 6250  quoremz 6251  intfracqOLD 6255  qrecclt 6273  seq1rn2 6321  ser1add2 6338  ser1add 6339  elioo3g 6380  elfz2t 6472  elfzlem 6473  elfz2nn0t 6495  fzaddelt 6500  fzrev2t 6512  fsequb 6523  seqzp1 6548  seqzrn2 6556  expeq0t 6585  expgt0t 6589  expgt1t 6592  mulexpt 6594  recexpt 6595  subsqt 6642  bernneq 6652  creur 6742  replimt 6761  cjexpt 6817  absexpt 6868  absmaxt 6897  cvganz 6924  facavgt 6955  fsumsplit 7020  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsumdivcALT 7036  fsumcmp0 7041  fsumcmpndx2 7042  serzmulc1 7057  bcxmas 7076  clm3 7079  clm4le 7081  climge0 7112  climaddlem3 7116  climaddc1 7118  climmullem8 7127  climmulc2 7129  climsubc2 7131  iserzmulc1 7136  climcmpc1 7139  climsqueeze 7140  climsqueeze2 7141  caucvglem2 7158  caucvglem4 7160  caucvglem5 7161  caucvglem6 7162  iserzgt0 7211  infcvglem3 7223  georeclim 7240  geoisumr 7243  geoisum1c 7245  cvgratlem1 7250  cncfval 7264  ivthlem7 7287  efaddlem10 7347  efaddlem23 7360  efaddlem25 7362  efexpt 7372  acdc2lem2 7489  acdc5lem2 7492  infmap2lem1 7579  infmap2lem2 7580  gch-kn 7587  basgen2t 7639  indistop 7648  fctopOLD 7650  cctop 7652  clscld 7683  elcls 7704  ntrcls0 7707  neii1 7721  neissex 7738  islp2 7747  ismsg 7800  meteq0 7812  blin 7852  blss 7853  opnfss 7858  lpbl 7880  metcnplem 7886  metcnpi3 7892  metcnpi4 7893  metcni2 7895  tgioolem 7914  dscmet 7918  lmbr 7928  lmnn 7935  lmuni 7951  lmsslem 7952  metelcls 7965  bcthlem8 8006  bcthlem10 8008  bcthlem17 8015  bcthlem26 8024  isgrp 8041  grpidinvlem2 8049  grpidinv 8052  grpinveu 8064  grpinv 8069  grpdivdiv 8087  grpmuldivass 8088  grppnpcan2 8092  abldivdiv4 8109  ringsn 8163  vcid 8170  vcdi 8171  vcdir 8172  nvzs 8265  nvmf 8266  nvmdi 8270  nvmtri2 8300  imsmetlem 8323  nmoub3i 8436  nmlno0lem 8453  nmblolbii 8459  ipdi 8503  ipassr 8506  ipsubdi 8509  ip2eqi 8517  ubthlem8 8536  ubthlem9 8537  ubthlem10 8538  ubthlem11 8539  pstr 8652  spwpr3OLD 8662  efif1lem3 8732  shftefif1olem 8741  hvaddsub4t 8945  norm1t 9121  norm1ex 9122  hhsscms 9150  chocuni 9172  occllem6 9178  projlem26 9211  pjtheu 9235  chabs1t 9439  normcant 9499  pjspansnt 9500  h1datom 9504  pjoml5t 9556  osumlem7 9584  5oalem1 9599  5oalem2 9600  5oalem5 9603  3oalem2 9608  pjidt 9640  pjds3 9658  nmopub2tALT 9833  cnvunopt 9842  unoplint 9844  counopt 9845  nmfnleub2t 9850  hmoplint 9866  nmlnop0ALT 9920  nmbdoplb 9949  nmcopexlem5 9955  nmcoplb 9958  nmbdfnlb 9978  nmcfnexlem5 9984  nmcfnlb 9987  riesz3 9995  riesz4 9996  cnlnadjeu 10010  adjlnopt 10019  branmfnt 10038  kbass5t 10053  leopsqt 10062  nmopleidt 10072  hmopidmpj 10080  pjclem4 10127  pj3s 10135  stge0t 10151  cvpsst 10212  ssmd2 10239  mdslj1 10246  mdslj2 10247  mdslmd1lem1 10252  mdslmd1lem2 10253  atcvat3 10323  atcvat4 10324  mdsymlem2 10331  mdsymlem3 10332  mdsymlem5 10334  cdj1 10360  hmphre 10530  hmeogrp 10538  fgsb 10570  fgsbOLD 10571  fgsb2 10580  rcfpfillem3 10589  rcfpfillem3OLD 10590  trnij 10637  homib 10724  icmpmon 10744  immon 10746  idfisf 10760

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