Theorem pm2.21i 123

Description: A contradiction implies anything. Inference from pm2.21 100. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
pm2.21i.1	⊢ ¬ φ

Assertion

Ref	Expression
pm2.21i	⊢ (φ → ψ)

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. . 3 ⊢ ¬ φ
2	1	a1i 10	. 2 ⊢ (¬ ψ → ¬ φ)
3	2	con4i 122	1 ⊢ (φ → ψ)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.24ii  124  pm3.2ni  827  falim  1328  nfnth  1556  ax4sp1  2174  rex0  3563  0ss  3579  abf  3584  r19.2zb  3640  ral0  3654  snsssn  3873  int0  3940  clos10  5887  po0  5939  connex0  5940  fnfreclem2  6318  fnfreclem3  6319