Theorem pm3.27 321

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 223	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2		pm3.27im 138	. 2 |- (-. (ph -> -. ps) -> ps)
3	1, 2	sylbi 197	1 |- ((ph /\ ps) -> ps)

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

This theorem is referenced by:  pm3.27i 322  pm3.27d 323  pm3.42 326  anclb 327  pm3.4 329  anim12i 331  ancom 437  imdistan 444  pm5.3 448  sylancom 478  anabs7 497  pm3.48 560  orabs 584  ordi 599  pm4.39 633  pm4.38 634  pm4.71 638  elimant 688  intnan 695  intnand 697  bianfi 742  pclem6 746  niabn 764  dedlem0b 766  19.26 1103  19.40 1130  equs4 1187  moan 1461  rexex 1739  r19.40 1808  rabab 1868  reu3 1977  difrab 2325  ifor 2435  preqsn 2551  intmin4 2626  intabs 2807  exss 2847  opelopab2 2896  suctr 3055  reuuni1 3106  eldifpw 3133  ordpwsuc 3172  nlimsucg 3196  ordunisuc2 3198  dfom2 3220  relop 3365  resiexg 3486  imassrn 3507  unielrel 3619  fun11uni 3670  dmfex 3762  tz6.12-2 3850  ssimaex 3879  fvopab6 3905  dffo3 3933  isofrlem 4015  2ndrn 4170  curry1val 4195  tfrlem5 4216  tz7.49 4260  oalim 4303  omlim 4304  oelim 4305  oaordex 4328  oalimcl 4330  oaass 4331  oneo 4348  nnaordex 4389  nnawordex 4390  eceqopreq 4454  pw2en 4587  ac6sfilem3 4590  ac6sfi 4591  sbthlem9 4600  suppr 4733  rankxplim3 4860  aceq4 4880  aceq5lem4 4884  aceq5lem5 4885  aceq6b 4888  ac6s3 4905  ac6s5 4908  kmlem2 4912  kmlem4 4914  unidom 4954  alephval3 5053  axrepndlem2 5099  axunnd 5102  axacndlem2 5114  axacndlem4 5116  axacnd 5118  mulcanpi 5181  indpi 5188  distrpqlem 5220  ltapq 5230  ltexpq 5234  ltexpq2 5235  ltbtwnpq 5238  genpnnp 5262  prlem934 5293  mulcmpblnr 5337  suppsr2 5377  pre-axsup 5445  cnegexlem1 5499  cnegex 5502  pncan3 5531  0re 5594  ltsubpos 5807  subge0 5828  recex 5840  lemul12aOLD 5987  lemul12a 5988  lt2mul2divOLD 6017  lediv2 6036  recreclt 6047  infmrcl 6237  xrsupexmnf 6242  xrinfmexpnf 6243  xrsupsslem 6244  xrinfmsslem 6245  supxrre 6251  elnnz1 6323  elnn0nn 6339  dfuzi 6373  uzindOLD 6379  zindd 6386  qreccl 6412  flwordi 6436  modid 6471  modabs 6473  modsubdir 6480  monoord 6482  iooval2 6493  elioo4g 6511  elioc2 6516  elico2 6517  elicc2 6518  ioojoin 6543  elfz2nn0 6625  fzelp1 6639  fzrev3i 6646  fzrevral 6650  fsequb 6654  ser1add2i 6703  ser1addi 6704  shftval5 6715  exprecOLD 6790  subsq 6839  nn0opthi 6867  creui 6944  rereb 6977  absmax 7100  cvg2i 7125  cvganz 7127  faclbnd3 7150  facavg 7158  fsumadd 7225  csbfsumlem 7229  fsumrev 7232  fsumdivcALT 7239  fsumcmp 7243  fsumcmp0 7244  serzmulc1 7260  binomlem6 7274  bcxmas 7279  clm3i 7282  clmi2i 7290  2climnn 7305  2climnn0 7306  climrecl 7313  climaddlem3 7319  climaddc1 7321  climmullem3 7325  climmullem8 7330  climsub 7333  climsubc2 7334  clim2serzi 7348  climserzlei 7350  caucvglem2 7361  caucvglem6 7365  serzf0i 7372  isumclim2f 7402  isum1p 7410  expcnv 7437  explecnv 7438  cvgratlem2ALT 7453  cvgratlem2 7456  fsum0diag3 7465  abscncflem 7479  ivthlem7 7492  efseq0ex 7516  efaddlem10 7552  efcn 7631  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  infxpidmlem8 7771  infxp 7784  infmap2lem2 7792  tpsex 7817  istps 7818  istps2 7819  tgcl 7836  tgval3 7837  topbas 7839  tgtop 7840  bastop 7845  tgss2 7849  basgen2 7851  bastop2 7855  subbas2 7857  indistop 7860  cctop 7862  opncld 7884  iincld 7889  elcls 7914  neii2 7932  neissex 7948  idcn 7976  cnpco 7979  cncnp 7988  cnconst 7990  mettri2 8023  mettri4 8024  blfval 8045  rnblssm 8061  blss 8063  ssblex 8066  opnin 8079  lpbl 8090  metequiv 8091  metcnplem 8097  metcnpi3 8103  metcnpi4 8104  metcni 8105  metcni2 8106  tgioolem 8125  lmcvg2 8144  lmuni 8162  lmss 8164  metelcls 8176  xplm 8186  bopcnlem2 8193  fsumcnlem 8200  iscms2lem4 8203  cncms 8209  bcthlem8 8217  bcthlem10 8219  bcthlem13 8222  bcthlem30 8239  grpidinvlem4 8264  grpidinv 8265  grpideu 8266  grprcan 8280  grpinvval 8284  isgrp2i 8293  grp2inv 8296  grpinvf 8297  gxinv 8326  gxsuc 8328  gxid 8329  gxadd 8331  gxnn0mul 8333  gxmul 8334  issubg 8358  subgabl 8365  ringideu 8387  ring2 8391  ringsn 8405  vcass 8420  vc0 8435  vcm 8437  vcoprnelem 8444  nvzs 8512  imsmetlem 8570  vacnlem5 8586  nmcnilem 8591  nmlno0lem 8708  blocni 8720  phpar2 8738  ipasslem4 8749  ip2eqi 8773  ubthlem6 8792  minveclem14 8818  htthlem10 8891  pstr 8914  spwpr4c 8928  lanfwcl 8931  hvaddsub4 9221  hi2eq 9247  normgt0OLD 9269  normgt0 9270  hcau2 9331  hhcms 9348  hhsscms 9426  chocunii 9448  projlem22 9483  pjop 9536  pjpo 9537  chssoc 9695  normcan 9775  pjspansn 9776  spanpr 9779  osumlem2 9857  spansncvi 9875  5oalem1 9877  5oalem2 9878  5oalem5 9881  3oalem2 9886  pjoi0 9940  unoplin 10124  counop 10125  elnlfn2 10133  hmoplin 10146  kbpj 10160  idcnop 10184  nmlnop0iALT 10199  nmcopexlem5 10234  lnopconi 10242  nmcfnexlem5 10263  lnfnconi 10269  lnfncnbd 10271  riesz3i 10274  riesz4i 10275  cnlnadjlem6 10284  adjlnop 10298  nmopadjlem 10301  rnbra 10320  leop2 10337  leopsq 10342  leopadd 10345  leopmuli 10346  leopnmid 10351  pjnmopi 10355  hmopidmchlem 10358  hmopidmchi 10359  pjhmopidm 10390  stle1 10433  hstles 10439  mdbr2 10504  dmdbr2 10511  mdslj1i 10527  mdslj2i 10528  mdsl2bi 10531  mdslmd1lem1 10533  mdslmd1lem2 10534  mdslmd4i 10541  cvdmd 10545  atom1d 10561  chrelat2i 10573  atcvatlem 10594  atcvat3i 10605  atcvat4i 10606  mdsymlem5 10616  sumdmdii 10624  cdj1i 10642  elo 10733  cmpfun 10751  inttr 10787  njtlc 10804  restidsing 10805  fiv 10849  ranncnt 10873  toplat 10884  opidon 10898  exidu1 10902  smgrpass 10913  rngmgmbs4 10945  zerab 10957  zerab2 10958  zrdivrng 10969  cdrci 10994  truni3 11001  oibbi1 11004  oibbi2 11005  mapudiscn 11015  sallnei 11016  hmeogrp 11044  stoig 11064  fgsb 11082  fgsb2 11086  cnfilca 11088  altretop 11144  msr3 11148  mslb1 11152  trnij 11160  cnvtr 11161  icmpmon 11271  idmon 11272  immon 11273  isepic 11279  simpllr 11363  simplrr 11365  simprlr 11367  simprrr 11369  elicc3 11410  ioodisj 11413  fictb 11423  finsschain 11425  ordiso 11426  ordtypelem6 11432  elomsubsd 11446  omsubinit 11451  opncldf2 11455  opncldf3 11456  ntrcmp 11458  clscmp 11459  opnregcld 11467  neiin 11470  cnpnei 11472  cncls 11473  subspid 11478  subsubtop 11479  cnsubsp2 11484  compcov 11486  cptclsscpt 11489  compfipin0 11493  cncomp 11494  connsub 11502  subtopmetlem 11505  subtopmet 11506  reconnlem4 11510  reconnlem5 11511  iccconn 11514  ivthALT 11515  is2ndc2 11534  isfne 11541  isref 11549  fnessref 11564  finlocfin 11570  locfincomp 11575  locfindsc 11576  comppfsc 11578  neibastop2lem1 11580  neibastop2lem4 11583  topmtcl 11586  topjoin 11588  fnejoin1 11591  fnejoin2 11592  fbfgss 11640  extbas1 11641  supfil 11645  isufil2 11650  ufprim 11654  ufileu 11658  uffixfr 11660  ufinffr 11663  hausfillim 11685  isfilmap 11689  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem2 11701  fmfnfmlem4 11703  fmfnfm 11704  fmufil 11705  filfm 11706  sflimf 11708  sfcls 11716  fcluscnplem 11729  sfclusf 11736  tailf 11756  istail 11757  filnetlem1 11763  filnetlem3 11765  filnetlem5 11767  filnet 11768  ssga 11777  gaass 11781  gapm 11784  fipreima 11848  divexp 11859  elnnr 11874  sdclem1 11875  nninfnub 11882  fsumlt1 11894  blssp 11908  metsstop 11909  mettrifi 11912  mettrifi2 11913  geomcau 11914  metdcn 11918  iccsplit 11919  addccncf 11945  sub1cncf 11946  sub2cncf 11947  hmeocnv 11959  tlmconst 11968  tx1cn 11976  tx2cn 11977  txcn 11979  sstotbnd 11992  isbnd3 11997  ismtybndlem 12008  heiborlem10 12020  heiborlem13 12023  heiborlem28 12038  heiborlem32 12042  heiborlem34 12044  heiborlem35 12045  heiborlem36 12046  bfplem8 12061  rrntotbndlem1 12076  phtpyid 12091  phtpycom 12092  phtpycolem3 12095  hgrablkne0 12199

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 145  df-an 223

Copyright terms: Public domain