Theorem pm2.21i 655

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

This theorem is referenced by:  pm2.24ii  656  2false  713  pm3.2ni  825  falim  1416  pclem6  1423  dcfromcon  1498  nfnth  1518  alnex  1552  ax4sp1  1586  rex0  3539  0ss  3561  abf  3569  ral0  3626  rabsnifsb  3773  int0  3979  nnsucelsuc  6754  nnmordi  6779  nnaordex  6791  0er  6831  fiintim  7228  elnnnn0b  9586  xltnegi  10216  xnn0xadd0  10248  frec2uzltd  10818  hashf1lem2  11264  sum0  12133  fsum2dlemstep  12179  prod0  12330  fprod2dlemstep  12367  nn0enne  12647  exprmfct  12894  prm23lt5  13020  4sqlem18  13165  0met  15408  lgsdir2lem3  16063  gausslemma2dlem0i  16090  2lgs  16137  2lgsoddprmlem3  16144  vtxdg0v  16449  clwwlkn0  16563  clwwlk0on0  16586