Theorem pm2.21i 73

Description: A contradiction implies anything. Inference from pm2.21 71.

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 7	. 2 ⊢ (¬ ψ → ¬ φ)
3	2	a3i 69	1 ⊢ (φ → ψ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  bianfi 553  rex0 1717  0ss 1725  rzal 1773  dtrucor 1890  int0 1978  po0 2137  so0 2153  fr0 2179  omordi 3164  omsmolem 3195  pssnn 3428  fiint 3445  alephordi 3679  nd1 3732  nd2 3733  nnsub 4450  om2uzlt 4654

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

metamath.org