Theorem pm2.21i 646

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

This theorem is referenced by:  pm2.24ii  647  2false  701  pm3.2ni  813  falim  1367  pclem6  1374  nfnth  1465  alnex  1499  ax4sp1  1533  rex0  3442  0ss  3463  abf  3468  ral0  3526  int0  3860  nnsucelsuc  6494  nnmordi  6519  nnaordex  6531  0er  6571  fiintim  6930  elnnnn0b  9222  xltnegi  9837  xnn0xadd0  9869  frec2uzltd  10405  sum0  11398  fsum2dlemstep  11444  prod0  11595  fprod2dlemstep  11632  nn0enne  11909  exprmfct  12140  prm23lt5  12265  0met  13969  lgsdir2lem3  14516  2lgsoddprmlem3  14544