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  6659  nnmordi  6684  nnaordex  6696  0er  6736  fiintim  7123  elnnnn0b  9446  xltnegi  10070  xnn0xadd0  10102  frec2uzltd  10666  sum0  11967  fsum2dlemstep  12013  prod0  12164  fprod2dlemstep  12201  nn0enne  12481  exprmfct  12728  prm23lt5  12854  4sqlem18  12999  0met  15127  lgsdir2lem3  15778  gausslemma2dlem0i  15805  2lgs  15852  2lgsoddprmlem3  15859  vtxdg0v  16164  clwwlkn0  16278  clwwlk0on0  16301