Theorem pm3.27 260

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 198	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2		pm3.27im 121	. 2 |- (-. (ph -> -. ps) -> ps)
3	1, 2	sylbi 174	1 |- ((ph /\ ps) -> ps)

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196

This theorem is referenced by:  pm3.27i 261  pm3.27d 262  anclb 264  pm3.4 266  anim12i 268  ancom 333  imdistan 339  anabs7 376  pm3.48 430  oel 441  ordi 452  pm4.71 481  msca 508  intnan 516  bianfi 553  pclem6 555  niabn 566  dedlem0b 568  19.26 749  19.40 773  moan 1046  rexex 1242  r19.40 1301  rabab 1359  difrab 1695  exss 1881  reuuni1 1955  ordelord 2221  onpwsuc 2315  dfom2 2374  imassrn 2611  fun11uni 2707  tz6.12-2 2845  f1fv 2916  isofrlem 2939  tfrlem5 2953  tz7.49 2997  oalim 3135  omlim 3136  oelim 3137  oaordex 3160  oalimcl 3162  oaass 3163  nnmordi 3188  nnaordex 3191  nnawordex 3192  omsmo 3196  ecopoprtrn 3247  eceqopreq 3249  pw2en 3348  sbthlem9 3357  sdomdomtr 3370  onomeneq 3414  aceq4 3557  aceq5lem4 3561  aceq5lem5 3562  aceq6b 3565  ac6s2 3578  kmlem2 3581  kmlem4 3583  axrepndlem2 3739  axunnd 3742  axacndlem2 3754  axacndlem4 3756  axacnd 3758  mulcanpi 3821  indpi 3828  distrpqlem 3860  ltapq 3870  ltexpq 3874  ltexpq2 3875  ltbtwnpq 3878  genpnnp 3902  prlem934 3933  mulcmpblnr 3977  mulgt0sr 4008  suppsr2 4017  axsup 4088  divmuldivt 4263  divadddivt 4264  divdiv23t 4271  ltsubpost 4364  creui 4533  elnnz1 4581  elnn0nn 4593  znnsubt 4595  uzind 4603  qrecclt 4646  nn0opth 4724  xpnnen 4927  infxpidmlem8 4940  infxpidmlem12 4944  infmap2lem2 4952  hvsubcan1t 5016  hvsubaddeqt 5019  hi2eqt 5059  normgt0t 5078  shmulclt 5124  ocorth 5172  chocuni 5179  projlem22 5214  projlem26 5218  pjthu2 5242  pjopt 5264  pjpot 5265  pjoml 5271  spansncol 5473  osumlem2 5531  osumlem6 5535  spansncv 5542  5oalem1 5544  5oalem2 5545  5oalem5 5548  3oalem2 5553  stle1t 5674  strlem3a 5693  mdbr2 5728  dmdbr2 5733  atom1d 5750  chrelat2 5758  cvp 5764  atcvatlem 5770  atcvat3 5774  atcvat4 5775  mdsymlem5 5780  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org