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  3564  0ss  3580  abf  3585  r19.2zb  3641  ral0  3655  snsssn  3874  int0  3941  clos10  5888  po0  5940  connex0  5941  fnfreclem2  6319  fnfreclem3  6320