Theorem pm2.21i 655

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

This theorem is referenced by:  pm2.24ii  656  2false  713  pm3.2ni  825  falim  1416  pclem6  1423  dcfromcon  1498  nfnth  1518  alnex  1552  ax4sp1  1586  rex0  3539  0ss  3561  abf  3570  ral0  3629  rabsnifsb  3776  int0  3982  nnsucelsuc  6758  nnmordi  6783  nnaordex  6795  0er  6835  fiintim  7232  elnnnn0b  9590  xltnegi  10220  xnn0xadd0  10252  frec2uzltd  10823  hashf1lem2  11269  sum0  12138  fsum2dlemstep  12184  prod0  12335  fprod2dlemstep  12372  nn0enne  12652  exprmfct  12899  prm23lt5  13025  4sqlem18  13170  0met  15468  lgsdir2lem3  16132  gausslemma2dlem0i  16159  2lgs  16206  2lgsoddprmlem3  16213  vtxdg0v  16518  clwwlkn0  16632  clwwlk0on0  16655