Theorem pm2.21i 613

Description: A contradiction implies anything. Inference from pm2.21 585. (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 585	. 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 583

This theorem is referenced by:  pm2.24ii  614  2false  655  pm3.2ni  765  falim  1310  pclem6  1317  nfnth  1406  alnex  1440  ax4sp1  1478  rex0  3319  0ss  3340  abf  3345  ral0  3403  int0  3724  nnsucelsuc  6292  nnmordi  6315  nnaordex  6326  0er  6366  fiintim  6719  elnnnn0b  8815  xltnegi  9401  xnn0xadd0  9433  frec2uzltd  9959  sum0  10947  fsum2dlemstep  10993  nn0enne  11345  exprmfct  11562  0met  12186