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  702  pm3.2ni  814  falim  1386  pclem6  1393  dcfromcon  1467  nfnth  1487  alnex  1521  ax4sp1  1555  rex0  3477  0ss  3498  abf  3503  ral0  3561  int0  3898  nnsucelsuc  6567  nnmordi  6592  nnaordex  6604  0er  6644  fiintim  7010  elnnnn0b  9321  xltnegi  9939  xnn0xadd0  9971  frec2uzltd  10529  sum0  11618  fsum2dlemstep  11664  prod0  11815  fprod2dlemstep  11852  nn0enne  12132  exprmfct  12379  prm23lt5  12505  4sqlem18  12650  0met  14774  lgsdir2lem3  15425  gausslemma2dlem0i  15452  2lgs  15499  2lgsoddprmlem3  15506