Theorem pm2.21i 647

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

This theorem is referenced by:  pm2.24ii  648  2false  703  pm3.2ni  815  falim  1387  pclem6  1394  dcfromcon  1469  nfnth  1489  alnex  1523  ax4sp1  1557  rex0  3482  0ss  3503  abf  3508  ral0  3566  int0  3905  nnsucelsuc  6590  nnmordi  6615  nnaordex  6627  0er  6667  fiintim  7043  elnnnn0b  9359  xltnegi  9977  xnn0xadd0  10009  frec2uzltd  10570  sum0  11774  fsum2dlemstep  11820  prod0  11971  fprod2dlemstep  12008  nn0enne  12288  exprmfct  12535  prm23lt5  12661  4sqlem18  12806  0met  14931  lgsdir2lem3  15582  gausslemma2dlem0i  15609  2lgs  15656  2lgsoddprmlem3  15663