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  3530  0ss  3551  abf  3556  ral0  3615  rabsnifsb  3762  int0  3968  nnsucelsuc  6737  nnmordi  6762  nnaordex  6774  0er  6814  fiintim  7204  elnnnn0b  9557  xltnegi  10187  xnn0xadd0  10219  frec2uzltd  10789  sum0  12099  fsum2dlemstep  12145  prod0  12296  fprod2dlemstep  12333  nn0enne  12613  exprmfct  12860  prm23lt5  12986  4sqlem18  13131  0met  15375  lgsdir2lem3  16029  gausslemma2dlem0i  16056  2lgs  16103  2lgsoddprmlem3  16110  vtxdg0v  16415  clwwlkn0  16529  clwwlk0on0  16552