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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-in2 624

This theorem is used 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  3777  int0  3984  relndmfv  5731  nnsucelsuc  6768  nnmordi  6793  nnaordex  6805  0er  6845  fiintim  7243  indval0  9307  elnnnn0b  9619  xltnegi  10255  xnn0xadd0  10287  frec2uzltd  10862  hashf1lem2  11309  sum0  12181  fsum2dlemstep  12227  prod0  12378  fprod2dlemstep  12415  nn0enne  12695  exprmfct  12943  prm23lt5  13072  4sqlem18  13217  prmlem1a  13251  prmlem2  13264  0met  15622  ppiublem1  16303  ppiublem2  16304  lgsdir2lem3  16366  gausslemma2dlem0i  16393  2lgs  16440  2lgsoddprmlem3  16447  vtxdg0v  16752  clwwlkn0  16866  clwwlk0on0  16889