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  1349  pclem6  1356  nfnth  1445  alnex  1479  ax4sp1  1513  rex0  3412  0ss  3433  abf  3438  ral0  3496  int0  3823  nnsucelsuc  6440  nnmordi  6465  nnaordex  6476  0er  6516  fiintim  6875  elnnnn0b  9139  xltnegi  9745  xnn0xadd0  9777  frec2uzltd  10311  sum0  11296  fsum2dlemstep  11342  prod0  11493  fprod2dlemstep  11530  nn0enne  11805  exprmfct  12030  prm23lt5  12153  0met  12854