Theorem pm3.27 323

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

Assertion

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

Proof of Theorem pm3.27

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

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

This theorem is referenced by:  pm3.27i 324  pm3.27d 325  pm3.42 328  anclb 329  pm3.4 331  anim12i 333  ancom 435  imdistan 442  pm5.3 446  anabs7 493  pm3.48 555  orabs 579  ordi 594  pm4.39 628  pm4.38 629  pm4.71 633  elimant 682  intnan 689  intnand 691  bianfi 735  pclem6 739  niabn 757  dedlem0b 759  19.26 1063  19.40 1090  equs4 1146  moan 1415  rexex 1685  r19.40 1754  rabab 1813  reu3 1921  difrab 2263  ifor 2371  preqsn 2477  intmin4 2549  intabs 2723  exss 2759  opelopab2 2808  reuuni1 2872  eldifpw 2900  ordpwsuc 3056  nlimsucg 3102  ordunisuc2 3105  dfom2 3123  relop 3265  resiexg 3380  imassrn 3399  unielrel 3500  fun11uni 3551  fnbr 3576  fimacnvdisj 3634  dmfex 3640  tz6.12-2 3724  ssimaex 3753  dffo3 3804  isofrlem 3886  tfrlem5 3900  tz7.49 3944  curry1val 4084  eqop 4088  2ndrn 4094  oalim 4151  omlim 4152  oelim 4153  oaordex 4176  oalimcl 4178  oaass 4179  oneo 4196  nnaordex 4233  nnawordex 4234  eceqopreq 4297  f1oeng 4376  pw2en 4426  sbthlem9 4435  onomeneq 4498  suppr 4562  rankxplim3 4686  aceq4 4706  aceq5lem4 4710  aceq5lem5 4711  aceq6b 4714  ac6s3 4731  ac6s5 4734  kmlem2 4738  kmlem4 4740  unidom 4780  alephval3 4875  axrepndlem2 4917  axunnd 4920  axacndlem2 4932  axacndlem4 4934  axacnd 4936  mulcanpi 4999  indpi 5006  distrpqlem 5038  ltapq 5048  ltexpq 5052  ltexpq2 5053  ltbtwnpq 5056  genpnnp 5080  prlem934 5111  mulcmpblnr 5155  suppsr2 5195  pre-axsup 5263  cnegextlem1 5317  cnegext 5320  pncan3t 5349  0re 5412  ltsubpost 5626  subge0t 5647  recext 5657  divcan5t 5737  divadddivt 5740  lemul12itOLD 5799  lemul12it 5800  lt2mul2divt 5822  lediv2t 5839  ltdiv23t 5840  lediv23t 5841  recrecltt 5850  avglet 5991  infmrcl 6016  xrsupexmnf 6021  xrinfmexpnf 6022  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  elnnz1 6102  elnn0nn 6118  dfuz 6150  uzindOLD 6156  flwordit 6183  monoord 6231  ser1add2 6275  ser1add 6276  shftval5t 6287  shftcan2t 6290  iooval2t 6304  elioo4g 6318  elioc2t 6322  elico2t 6323  elicc2t 6324  elfz2nn0t 6427  fzelp1t 6440  fzrev3it 6447  fzneuzt 6450  fzrevralt 6451  fsequb 6455  recexpt 6526  subsqt 6573  nn0opth 6596  creui 6674  cvg2 6859  cvganz 6861  faclbnd3 6884  facavgt 6892  fsumadd 6960  csbfsumlem 6964  fsumrev 6967  fsumdivcALT 6974  fsumcmp 6978  fsumcmp0 6979  serzmulc1 6995  binomlem6 7009  bcxmas 7014  clm3 7017  clmi2 7025  2climnn 7039  2climnn0 7040  climrecl 7047  climaddlem3 7052  climaddc1 7054  climmullem3 7058  climmullem8 7063  climsub 7066  climsubc2 7067  clim2serz 7081  climserzle 7083  caucvglem2 7094  caucvglem6 7098  serzf0 7105  ser1f0 7106  isumclim2tf 7133  isum1p 7141  expcnv 7168  geoisum1c 7180  cvgratlem2 7186  fsum0diag3 7195  abscncflem 7209  ivthlem7 7222  ivthlem7OLD 7231  efseq0ex 7253  efaddlem10 7289  efaddlem23 7302  efcn 7363  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  xpnnen 7441  infxpidmlem8 7502  infxpidmlem12 7506  infxp 7515  infmap2lem2 7522  tpsex 7547  istps 7548  istps2 7549  tgclt 7566  tgval3t 7567  topbast 7569  tgtopt 7570  bastopt 7575  tgss2t 7579  basgen2t 7581  bastop2 7585  subbas2 7587  indistop 7590  cctop 7594  opncld 7616  iincld 7621  elcls 7646  neii2 7663  neissex 7679  idcn 7705  cnpco 7708  cncnp 7717  cnconst 7719  mettri2 7752  mettri4 7753  blfval 7775  rnblssm 7791  blss 7793  ssblex 7796  opnin 7809  lpbl 7819  metcnplem 7825  metcnpi3 7831  metcnpi4 7832  metcni 7833  metcni2 7834  tgioolem 7853  lmcvg2 7871  lmuni 7886  lmss 7888  metelcls 7900  xplm 7909  bopcnlem2 7916  fsumcnlem 7923  iscms2lem4 7926  cmsss 7931  cncms 7932  bcthlem8 7940  bcthlem10 7942  bcthlem13 7945  bcthlem30 7962  grpidinvlem4 7985  grpidinv 7986  grpideu 7987  grprcan 7997  grpinvval 8001  isgrp2i 8011  grp2inv 8013  grpinvf 8014  issubg 8053  subgabl 8060  ring2 8086  ringsn 8100  vcass 8110  vc0 8125  vcm 8127  vcoprnelem 8135  nvzs 8205  imsmetlem 8261  nmcnilem 8272  nmlno0lem 8385  blocni 8396  phpar2 8413  ipasslem1 8421  ipasslem4 8424  ip2eqi 8448  ubthlem6 8465  minveclem14 8489  htthlem10 8559  hvpncant 8829  hvaddsub4t 8866  hi2eqt 8892  normgt0tOLD 8914  normgt0t 8915  hcau2 8976  hhcms 8993  hhsscms 9067  chocuni 9088  projlem22 9123  pjopt 9175  pjpot 9176  chssoct 9334  normcant 9416  pjspansnt 9417  spanpr 9420  osumlem2 9496  spansncv 9514  5oalem1 9516  5oalem2 9517  5oalem5 9520  3oalem2 9525  pjidt 9557  pjoi0t 9579  unoplint 9760  counopt 9761  hmopret 9763  elnlfn2t 9769  hmoplint 9782  kbpjt 9796  eigvalclt 9801  idcnop 9821  nmlnop0ALT 9835  nmcopexlem5 9870  lnopcon 9878  nmcfnexlem5 9899  lnfncon 9905  lnfncnbdt 9907  riesz3 9910  riesz4 9911  cnlnadjlem6 9920  adjlnopt 9934  nmopadjlem 9937  rnbra 9953  leop2t 9969  leopsqt 9974  leopaddt 9977  leopmulit 9978  leopnmidt 9982  pjnmop 9986  hmopidmchlem 9989  hmopidmch 9990  pjhmopidm 10020  stle1t 10062  hstlest 10068  mdbr2 10133  dmdbr2 10140  mdslj1 10154  mdslj2 10155  mdsl2b 10158  mdslmd1lem1 10160  mdslmd1lem2 10161  mdslmd4 10168  cvdmdt 10172  atom1d 10188  superpos 10189  chrelat2 10200  cvp 10210  atcvatlem 10220  atcvat3 10231  atcvat4 10232  mdsymlem5 10242  sumdmdi 10249  cdj1 10265  elo 10345  cmpfun 10363  fiv 10374  cdrci 10381  mapudiscn 10399  hmeogrp 10425  fgsb 10444  fgsb2 10449  cnfilca 10451  msr3 10469  mslb1 10473  trnij 10481  cnvtr 10482  icmpmon 10587  idmon 10588  immon 10589  hgrablkne0 10609

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