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  708  pm3.2ni  820  falim  1411  pclem6  1418  dcfromcon  1493  nfnth  1513  alnex  1547  ax4sp1  1581  rex0  3512  0ss  3533  abf  3538  ral0  3596  rabsnifsb  3737  int0  3942  nnsucelsuc  6658  nnmordi  6683  nnaordex  6695  0er  6735  fiintim  7122  elnnnn0b  9445  xltnegi  10069  xnn0xadd0  10101  frec2uzltd  10664  sum0  11948  fsum2dlemstep  11994  prod0  12145  fprod2dlemstep  12182  nn0enne  12462  exprmfct  12709  prm23lt5  12835  4sqlem18  12980  0met  15107  lgsdir2lem3  15758  gausslemma2dlem0i  15785  2lgs  15832  2lgsoddprmlem3  15839  vtxdg0v  16144  clwwlkn0  16258  clwwlk0on0  16281