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  3514  0ss  3535  abf  3540  ral0  3598  rabsnifsb  3741  int0  3947  nnsucelsuc  6702  nnmordi  6727  nnaordex  6739  0er  6779  fiintim  7166  elnnnn0b  9488  xltnegi  10114  xnn0xadd0  10146  frec2uzltd  10711  sum0  12012  fsum2dlemstep  12058  prod0  12209  fprod2dlemstep  12246  nn0enne  12526  exprmfct  12773  prm23lt5  12899  4sqlem18  13044  0met  15178  lgsdir2lem3  15832  gausslemma2dlem0i  15859  2lgs  15906  2lgsoddprmlem3  15913  vtxdg0v  16218  clwwlkn0  16332  clwwlk0on0  16355