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  dcfromcon  1459  nfnth  1479  alnex  1513  ax4sp1  1547  rex0  3469  0ss  3490  abf  3495  ral0  3553  int0  3889  nnsucelsuc  6558  nnmordi  6583  nnaordex  6595  0er  6635  fiintim  7001  elnnnn0b  9310  xltnegi  9927  xnn0xadd0  9959  frec2uzltd  10512  sum0  11570  fsum2dlemstep  11616  prod0  11767  fprod2dlemstep  11804  nn0enne  12084  exprmfct  12331  prm23lt5  12457  4sqlem18  12602  0met  14704  lgsdir2lem3  15355  gausslemma2dlem0i  15382  2lgs  15429  2lgsoddprmlem3  15436