Theorem pm2.21i 635

Description: A contradiction implies anything. Inference from pm2.21 606. (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 606	. 2 |- ( -. ph -> ( ph -> ps ) )
3	1, 2	ax-mp 5	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-in2 604

This theorem is referenced by:  pm2.24ii  636  2false  690  pm3.2ni  802  falim  1345  pclem6  1352  nfnth  1441  alnex  1475  ax4sp1  1513  rex0  3380  0ss  3401  abf  3406  ral0  3464  int0  3785  nnsucelsuc  6387  nnmordi  6412  nnaordex  6423  0er  6463  fiintim  6817  elnnnn0b  9021  xltnegi  9618  xnn0xadd0  9650  frec2uzltd  10176  sum0  11157  fsum2dlemstep  11203  nn0enne  11599  exprmfct  11818  0met  12553