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 690  intnanrd 692  biantrud 724  bianfd 736  pm5.75 747  dedlemb 761  nicodraw 949  19.26 1063  19.40 1090  sbequ2 1175  mopick2 1429  moexex 1431  2exeu 1439  2eu2 1443  r19.40 1754  reu3 1921  csbnestglem 2025  csbnest1g 2027  ssab2 2120  uneqin 2246  difprsn 2456  unissel 2517  ssmin 2542  iununi 2606  class2set 2724  moabex 2756  mosubopt 2793  ordsseleq 2966  onin 2968  ordsson 2981  opelxp 3204  ralxp 3208  xpss 3220  opabssxp 3224  dmcosseq 3349  relssres 3376  dminss 3448  cores 3485  fun11uni 3551  dffo4 3805  ffnfv 3813  isotr 3882  isotrALT 3883  isofrlem 3886  f1oiso 3889  tfrlem8 3903  tz7.48lem 3940  fnoprabg 3997  eloprabi 4102  omordi 4181  omord 4183  omlimcl 4193  oneo 4196  oen0 4197  oeordi 4198  oewordri 4203  oeordsuc 4205  eceqopreq 4297  th3qlem1 4298  pw2en 4426  ssenen 4484  unblem2 4518  dfom3 4602  r1ord 4627  r1val1 4630  rankr1 4646  rankuni 4670  rankxplim3 4686  karden 4698  hta 4700  aceq3 4705  kmlem8 4744  kmlem16 4752  brdom7disj 4776  brdom6disj 4777  unidom 4780  cardalephex 4858  axunnd 4920  axacndlem1 4931  axacndlem3 4933  enqeceq 5019  distrpq 5039  genpnnp 5080  addclprlem2 5091  distrlem4pr 5102  prlem936 5127  reclem3pr 5130  suplem2pr 5134  enreceq 5149  mulcmpblnr 5155  pncan3t 5349  0re 5412  leltnet 5494  xrleltnet 5531  ltsubpost 5626  posdift 5627  subge0t 5647  recextlem1 5655  recid2t 5699  divcan5t 5737  divdivdivt 5741  divdivmult 5751  ltmul12it 5797  lemul12itOLD 5799  mulgt1t 5801  lt2mul2divt 5822  ltdiv2t 5835  ledivdivt 5838  lediv2t 5839  recp1lt1 5849  recrecltt 5850  ledivp1t 5853  1nn 5882  nnleltp1t 5901  avglet 5991  nnreclt 6019  flwordit 6183  ceilet 6193  qrecclt 6211  seq1rn2 6258  ser1add2 6275  ser1add 6276  elioo3g 6317  elfz2t 6404  elfzlem 6405  elfz2nn0t 6427  fzaddelt 6432  fzrev2t 6444  fsequb 6455  seqzp1 6480  seqzrn2 6488  expeq0t 6517  expgt0t 6520  expgt1t 6523  mulexpt 6525  recexpt 6526  subsqt 6573  bernneq 6583  creur 6673  replimt 6692  cjexpt 6752  absexpt 6803  cvganz 6861  facavgt 6892  fsumsplit 6958  fsumadd 6960  fsumcom 6966  fsumrev 6967  fsumdivcALT 6974  fsumcmp0 6979  fsumcmpndx2 6980  serzmulc1 6995  bcxmas 7014  clm3 7017  clm4le 7019  climge0 7049  climaddlem3 7052  climaddc1 7054  climmullem8 7063  climmulc2 7065  climsubc2 7067  iserzmulc1 7072  climcmpc1 7075  climsqueeze 7076  climsqueeze2 7077  caucvglem2 7094  caucvglem4 7096  caucvglem5 7097  caucvglem6 7098  iserzgt0 7146  infcvglem3 7158  georeclim 7175  geoisumr 7178  geoisum1c 7180  cvgratlem1 7185  cncfval 7199  ivthlem7 7222  ivthlem7OLD 7231  efaddlem10 7289  efaddlem23 7302  efaddlem25 7304  efexpt 7314  acdc2lem2 7431  acdc5lem2 7434  infmap2lem1 7521  infmap2lem2 7522  gch-kn 7529  basgen2t 7581  indistop 7590  fctop 7592  cctop 7594  clscld 7625  elcls 7646  ntrcls0 7649  neii1 7662  neissex 7679  islp2 7688  ismsg 7739  meteq0 7751  blin 7792  blss 7793  opnfss 7798  lpbl 7819  metcnplem 7825  metcnpi3 7831  metcnpi4 7832  metcni2 7834  tgioolem 7853  dscmet 7856  lmbr 7866  lmnn 7873  lmuni 7886  lmsslem 7887  metelcls 7900  bcthlem8 7940  bcthlem10 7942  bcthlem17 7949  bcthlem26 7958  isgrp 7975  grpidinvlem2 7983  grpidinv 7986  grpinveu 7998  grpinv 8003  grpdivdiv 8022  grpmuldivass 8023  grppnpcan2 8027  abldivdiv4 8046  ringsn 8100  vcid 8107  vcdi 8108  vcdir 8109  nvzs 8205  nvmf 8206  nvmdi 8210  nvmtri2 8239  imsmetlem 8261  nmoub3i 8368  nmlno0lem 8385  nmblolbii 8390  ipdi 8434  ipassr 8437  ipsubdi 8440  ip2eqi 8448  ubthlem8 8467  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  efif1lem3 8647  shftefif1olem 8661  shftefif1olemOLD 8662  hvaddsub4t 8866  norm1t 9042  norm1ex 9043  hhsscms 9067  chocuni 9088  occllem6 9094  projlem26 9127  pjtheu 9150  chabs1t 9354  normcant 9416  pjspansnt 9417  h1datom 9421  pjoml5t 9473  osumlem7 9501  5oalem1 9516  5oalem2 9517  5oalem5 9520  3oalem2 9525  pjidt 9557  pjds3 9575  nmopub2tALT 9750  cnvunopt 9758  unoplint 9760  counopt 9761  nmfnleub2t 9766  hmoplint 9782  nmlnop0ALT 9835  nmbdoplb 9864  nmcopexlem5 9870  nmcoplb 9873  nmbdfnlb 9893  nmcfnexlem5 9899  nmcfnlb 9902  riesz3 9910  riesz4 9911  cnlnadjeu 9925  adjlnopt 9934  branmfnt 9951  kbass5t 9965  leopsqt 9974  nmopleidt 9983  hmopidmpj 9991  pjclem4 10037  pj3s 10045  stge0t 10061  cvpsst 10122  ssmd2 10147  mdslj1 10154  mdslj2 10155  mdslmd1lem1 10160  mdslmd1lem2 10161  atcvat3 10231  atcvat4 10232  mdsymlem2 10239  mdsymlem3 10240  mdsymlem5 10242  cdj1 10265  hmphre 10417  hmeogrp 10425  fgsb 10444  fgsb2 10449  trnij 10481  homib 10568  icmpmon 10587  immon 10589

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