Theorem pm2.21i 575

Description: A contradiction implies anything. Inference from pm2.21 547. (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 547	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	ax-mp 7	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 7  ax-in2 545

This theorem is referenced by:  pm2.24ii  576  2false  617  pm3.2ni  726  falim  1257  pclem6  1265  nfnth  1354  alnex  1388  ax4sp1  1426  rex0  3238  0ss  3255  abf  3260  ral0  3322  int0  3629  nnsucelsuc  6070  nnmordi  6089  nnaordex  6100  0er  6140  elnnnn0b  8226  xltnegi  8748  frec2uzltd  9189