Theorem pm2.21i 636

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

This theorem is referenced by:  pm2.24ii  637  2false  691  pm3.2ni  803  falim  1357  pclem6  1364  nfnth  1453  alnex  1487  ax4sp1  1521  rex0  3425  0ss  3446  abf  3451  ral0  3509  int0  3837  nnsucelsuc  6455  nnmordi  6480  nnaordex  6491  0er  6531  fiintim  6890  elnnnn0b  9154  xltnegi  9767  xnn0xadd0  9799  frec2uzltd  10334  sum0  11325  fsum2dlemstep  11371  prod0  11522  fprod2dlemstep  11559  nn0enne  11835  exprmfct  12066  prm23lt5  12191  0met  12984  lgsdir2lem3  13531