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  1463  alnex  1497  ax4sp1  1531  rex0  3438  0ss  3459  abf  3464  ral0  3522  int0  3854  nnsucelsuc  6482  nnmordi  6507  nnaordex  6519  0er  6559  fiintim  6918  elnnnn0b  9191  xltnegi  9804  xnn0xadd0  9836  frec2uzltd  10371  sum0  11362  fsum2dlemstep  11408  prod0  11559  fprod2dlemstep  11596  nn0enne  11872  exprmfct  12103  prm23lt5  12228  0met  13435  lgsdir2lem3  13982