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	⊢ ¬ 𝜑

Assertion

Ref	Expression
pm2.21i	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. 2 ⊢ ¬ 𝜑
2		pm2.21 622	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → 𝜓)

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  3511  0ss  3532  abf  3537  ral0  3595  rabsnifsb  3738  int0  3943  nnsucelsuc  6664  nnmordi  6689  nnaordex  6701  0er  6741  fiintim  7128  elnnnn0b  9451  xltnegi  10075  xnn0xadd0  10107  frec2uzltd  10671  sum0  11972  fsum2dlemstep  12018  prod0  12169  fprod2dlemstep  12206  nn0enne  12486  exprmfct  12733  prm23lt5  12859  4sqlem18  13004  0met  15137  lgsdir2lem3  15788  gausslemma2dlem0i  15815  2lgs  15862  2lgsoddprmlem3  15869  vtxdg0v  16174  clwwlkn0  16288  clwwlk0on0  16311