Theorem pm2.65i 185

Description: Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
pm2.65i.1	|- ( ph -> ps )
pm2.65i.2	|- ( ph -> -. ps )

Assertion

Ref	Expression
pm2.65i	|- -. ph

Proof of Theorem pm2.65i

Step	Hyp	Ref	Expression
1		pm2.65i.2	. . 3 |- ( ph -> -. ps )
2	1	con2i 134	. 2 |- ( ps -> -. ph )
3		pm2.65i.1	. . 3 |- ( ph -> ps )
4	3	con3i 150	. 2 |- ( -. ps -> -. ph )
5	2, 4	pm2.61i 176	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4

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

This theorem is referenced by:  pm2.21dd  186  mto  188  mt2  191  noel  3919  0nelop  4960  canth  6608  sdom0  8092  canthwdom  8484  cardprclem  8805  ominf4  9134  canthp1lem2  9475  pwfseqlem4  9484  pwxpndom2  9487  lbioo  12206  ubioo  12207  fzp1disj  12399  fzonel  12483  fzouzdisj  12504  hashbclem  13236  harmonic  14591  eirrlem  14932  ruclem13  14971  prmreclem6  15625  4sqlem17  15665  vdwlem12  15696  vdwnnlem3  15701  mreexmrid  16303  psgnunilem3  17916  efgredlemb  18159  efgredlem  18160  00lss  18942  alexsublem  21848  ptcmplem4  21859  nmoleub2lem3  22915  dvferm1lem  23747  dvferm2lem  23749  plyeq0lem  23966  logno1  24382  lgsval2lem  25032  pntpbnd2  25276  ubico  29537  bnj1523  31139  pm2.65ni  39210  lbioc  39739  salgencntex  40561