Theorem pm2.21i 607

Description: A contradiction implies anything. Inference from pm2.21 579. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
pm2.21i.1	|- -. ph

Assertion

Ref	Expression
pm2.21i	|- ( ph -> ps )

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. 2 |- -. ph
2		pm2.21 579	. 2 |- ( -. ph -> ( ph -> ps ) )
3	1, 2	ax-mp 7	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 7  ax-in2 577

This theorem is referenced by:  pm2.24ii  608  2false  649  pm3.2ni  759  falim  1298  pclem6  1305  nfnth  1394  alnex  1428  ax4sp1  1466  rex0  3265  0ss  3282  abf  3287  ral0  3342  int0  3650  nnsucelsuc  6093  nnmordi  6112  nnaordex  6123  0er  6163  elnnnn0b  8332  xltnegi  8902  frec2uzltd  9405  nn0enne  10302  exprmfct  10519