Theorem pm2.21i 647

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

This theorem is referenced by:  pm2.24ii  648  2false  702  pm3.2ni  814  falim  1378  pclem6  1385  nfnth  1476  alnex  1510  ax4sp1  1544  rex0  3455  0ss  3476  abf  3481  ral0  3539  int0  3873  nnsucelsuc  6516  nnmordi  6541  nnaordex  6553  0er  6593  fiintim  6957  elnnnn0b  9250  xltnegi  9865  xnn0xadd0  9897  frec2uzltd  10434  sum0  11428  fsum2dlemstep  11474  prod0  11625  fprod2dlemstep  11662  nn0enne  11939  exprmfct  12170  prm23lt5  12295  4sqlem18  12440  0met  14344  lgsdir2lem3  14892  2lgsoddprmlem3  14920