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  1346  pclem6  1353  nfnth  1442  alnex  1476  ax4sp1  1514  rex0  3385  0ss  3406  abf  3411  ral0  3469  int0  3793  nnsucelsuc  6395  nnmordi  6420  nnaordex  6431  0er  6471  fiintim  6825  elnnnn0b  9045  xltnegi  9648  xnn0xadd0  9680  frec2uzltd  10207  sum0  11189  fsum2dlemstep  11235  nn0enne  11635  exprmfct  11854  0met  12592