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  sylancom 475  anabs7 494  pm3.48 556  orabs 580  ordi 595  pm4.39 629  pm4.38 630  pm4.71 634  elimant 683  intnan 690  intnand 692  bianfi 736  pclem6 740  niabn 758  dedlem0b 760  19.26 1065  19.40 1092  equs4 1148  moan 1420  rexex 1690  r19.40 1759  rabab 1818  reu3 1927  difrab 2269  ifor 2377  preqsn 2482  intmin4 2554  intabs 2728  exss 2764  opelopab2 2814  reuuni1 2877  eldifpw 2905  ordpwsuc 3061  nlimsucg 3107  ordunisuc2 3110  dfom2 3128  relop 3270  resiexg 3388  imassrn 3407  unielrel 3506  fun11uni 3557  dmfex 3646  tz6.12-2 3730  ssimaex 3759  dffo3 3810  isofrlem 3892  tfrlem5 3906  tz7.49 3950  curry1val 4090  2ndrn 4100  oalim 4157  omlim 4158  oelim 4159  oaordex 4182  oalimcl 4184  oaass 4185  oneo 4202  nnaordex 4239  nnawordex 4240  eceqopreq 4303  pw2en 4432  sbthlem9 4441  suppr 4570  rankxplim3 4694  aceq4 4714  aceq5lem4 4718  aceq5lem5 4719  aceq6b 4722  ac6s3 4739  ac6s5 4742  kmlem2 4746  kmlem4 4748  unidom 4788  alephval3 4883  axrepndlem2 4925  axunnd 4928  axacndlem2 4940  axacndlem4 4942  axacnd 4944  mulcanpi 5007  indpi 5014  distrpqlem 5046  ltapq 5056  ltexpq 5060  ltexpq2 5061  ltbtwnpq 5064  genpnnp 5088  prlem934 5119  mulcmpblnr 5163  suppsr2 5203  pre-axsup 5271  cnegextlem1 5325  cnegext 5328  pncan3t 5357  0re 5420  ltsubpost 5634  subge0t 5655  recext 5665  divcan5t 5745  divadddivt 5748  lemul12itOLD 5807  lemul12it 5808  lt2mul2divt 5830  lediv2t 5847  recrecltt 5858  infmrcl 6024  xrsupexmnf 6029  xrinfmexpnf 6030  xrsupsslem 6031  xrinfmsslem 6032  supxrre 6038  elnnz1 6110  elnn0nn 6126  dfuz 6158  uzindOLD 6164  flwordit 6191  monoord 6239  ser1add2 6283  ser1add 6284  shftval5t 6295  iooval2t 6312  elioo4g 6326  elioc2t 6330  elico2t 6331  elicc2t 6332  elfz2nn0t 6435  fzelp1t 6448  fzrev3it 6455  fzrevralt 6459  fsequb 6463  recexpt 6534  subsqt 6581  nn0opth 6604  creui 6682  cvg2 6867  cvganz 6869  faclbnd3 6892  facavgt 6900  fsumadd 6968  csbfsumlem 6972  fsumrev 6975  fsumdivcALT 6982  fsumcmp 6986  fsumcmp0 6987  serzmulc1 7003  binomlem6 7017  bcxmas 7022  clm3 7025  clmi2 7033  2climnn 7047  2climnn0 7048  climrecl 7055  climaddlem3 7060  climaddc1 7062  climmullem3 7066  climmullem8 7071  climsub 7074  climsubc2 7075  clim2serz 7089  climserzle 7091  caucvglem2 7102  caucvglem6 7106  serzf0 7113  ser1f0 7114  isumclim2tf 7141  isum1p 7149  expcnv 7176  geoisum1c 7188  cvgratlem2 7194  fsum0diag3 7203  abscncflem 7217  ivthlem7 7230  ivthlem7OLD 7239  efseq0ex 7261  efaddlem10 7297  efaddlem23 7310  efcn 7371  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  infxpidmlem8 7510  infxp 7523  infmap2lem2 7530  tpsex 7555  istps 7556  istps2 7557  tgclt 7574  tgval3t 7575  topbast 7577  tgtopt 7578  bastopt 7583  tgss2t 7587  basgen2t 7589  bastop2 7593  subbas2 7595  indistop 7598  cctop 7602  opncld 7624  iincld 7629  elcls 7654  neii2 7672  neissex 7688  idcn 7716  cnpco 7719  cncnp 7728  cnconst 7730  mettri2 7763  mettri4 7764  blfval 7787  rnblssm 7803  blss 7805  ssblex 7808  opnin 7821  lpbl 7832  metcnplem 7838  metcnpi3 7844  metcnpi4 7845  metcni 7846  metcni2 7847  tgioolem 7866  lmcvg2 7885  lmuni 7902  lmss 7904  metelcls 7916  xplm 7925  bopcnlem2 7932  fsumcnlem 7939  iscms2lem4 7942  cncms 7948  bcthlem8 7956  bcthlem10 7958  bcthlem13 7961  bcthlem30 7978  grpidinvlem4 8001  grpidinv 8002  grpideu 8003  grprcan 8013  grpinvval 8017  isgrp2i 8026  grp2inv 8028  grpinvf 8029  issubg 8068  subgabl 8075  ring2 8101  ringsn 8115  vcass 8125  vc0 8140  vcm 8142  vcoprnelem 8149  nvzs 8217  imsmetlem 8274  nmcnilem 8285  nmlno0lem 8398  blocni 8409  phpar2 8426  ipasslem4 8437  ip2eqi 8461  ubthlem6 8478  minveclem14 8502  htthlem10 8572  pstr 8594  hvaddsub4t 8884  hi2eqt 8910  normgt0tOLD 8932  normgt0t 8933  hcau2 8994  hhcms 9011  hhsscms 9089  chocuni 9111  projlem22 9146  pjopt 9198  pjpot 9199  chssoct 9357  normcant 9439  pjspansnt 9440  spanpr 9443  osumlem2 9519  spansncv 9537  5oalem1 9539  5oalem2 9540  5oalem5 9543  3oalem2 9548  pjoi0t 9602  unoplint 9783  counopt 9784  elnlfn2t 9792  hmoplint 9805  kbpjt 9819  idcnop 9844  nmlnop0ALT 9858  nmcopexlem5 9893  lnopcon 9901  nmcfnexlem5 9922  lnfncon 9928  lnfncnbdt 9930  riesz3 9933  riesz4 9934  cnlnadjlem6 9943  adjlnopt 9957  nmopadjlem 9960  rnbra 9978  leop2t 9995  leopsqt 10000  leopaddt 10003  leopmulit 10004  leopnmidt 10009  pjnmop 10013  hmopidmchlem 10016  hmopidmch 10017  pjhmopidm 10048  stle1t 10090  hstlest 10096  mdbr2 10161  dmdbr2 10168  mdslj1 10183  mdslj2 10184  mdsl2b 10187  mdslmd1lem1 10189  mdslmd1lem2 10190  mdslmd4 10197  cvdmdt 10201  atom1d 10217  chrelat2 10229  atcvatlem 10249  atcvat3 10260  atcvat4 10261  mdsymlem5 10271  sumdmdi 10278  cdj1 10294  elo 10381  cmpfun 10399  fiv 10410  cdrci 10417  mapudiscn 10435  hmeogrp 10461  fgsb 10480  fgsb2 10485  cnfilca 10487  msr3 10505  mslb1 10509  trnij 10517  cnvtr 10518  icmpmon 10623  idmon 10624  immon 10625  hgrablkne0 10645

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