Theorem pm2.65i 640

Description: Inference 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		pm2.65i.1	. . 3 |- ( ph -> ps )
3	1, 2	nsyl3 627	. 2 |- ( ph -> -. ph )
4		pm2.01 617	. 2 |- ( ( ph -> -. ph ) -> -. ph )
5	3, 4	ax-mp 5	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 615  ax-in2 616

This theorem is referenced by:  mt2  641  mto  664  pm5.19  708  noel  3472  0nelop  4310  elirr  4607  en2lp  4620  soirri  5096  canth  5920  0neqopab  6013  fzp1disj  10237  fzonel  10318  fzouzdisj  10339  4sqlem17  12845  lgsval2lem  15602  bj-imnimnn  15874  nnnotnotr  16125