Theorem pm2.21i 649

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

This theorem is referenced by:  pm2.24ii  650  2false  706  pm3.2ni  818  falim  1409  pclem6  1416  dcfromcon  1491  nfnth  1511  alnex  1545  ax4sp1  1579  rex0  3510  0ss  3531  abf  3536  ral0  3594  rabsnifsb  3735  int0  3940  nnsucelsuc  6654  nnmordi  6679  nnaordex  6691  0er  6731  fiintim  7118  elnnnn0b  9439  xltnegi  10063  xnn0xadd0  10095  frec2uzltd  10658  sum0  11942  fsum2dlemstep  11988  prod0  12139  fprod2dlemstep  12176  nn0enne  12456  exprmfct  12703  prm23lt5  12829  4sqlem18  12974  0met  15101  lgsdir2lem3  15752  gausslemma2dlem0i  15779  2lgs  15826  2lgsoddprmlem3  15833  vtxdg0v  16105  clwwlkn0  16217  clwwlk0on0  16240