Theorem pm2.21i 651

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

This theorem is referenced by:  pm2.24ii  652  2false  709  pm3.2ni  821  falim  1412  pclem6  1419  dcfromcon  1494  nfnth  1514  alnex  1548  ax4sp1  1582  rex0  3526  0ss  3547  abf  3552  ral0  3611  rabsnifsb  3757  int0  3963  nnsucelsuc  6724  nnmordi  6749  nnaordex  6761  0er  6801  fiintim  7191  elnnnn0b  9540  xltnegi  10168  xnn0xadd0  10200  frec2uzltd  10765  sum0  12074  fsum2dlemstep  12120  prod0  12271  fprod2dlemstep  12308  nn0enne  12588  exprmfct  12835  prm23lt5  12961  4sqlem18  13106  0met  15249  lgsdir2lem3  15903  gausslemma2dlem0i  15930  2lgs  15977  2lgsoddprmlem3  15984  vtxdg0v  16289  clwwlkn0  16403  clwwlk0on0  16426