Theorem con1i 88

Description: A contraposition inference.

Hypothesis

Ref	Expression
con1.a	⊢ (¬ φ → ψ)

Assertion

Ref	Expression
con1i	⊢ (¬ ψ → φ)

Proof of Theorem con1i

Step	Hyp	Ref	Expression
1		con1.a	. . 3 ⊢ (¬ φ → ψ)
2		negb 79	. . 3 ⊢ (ψ → ¬ ¬ ψ)
3	1, 2	syl 12	. 2 ⊢ (¬ φ → ¬ ¬ ψ)
4	3	a3i 69	1 ⊢ (¬ ψ → φ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  con3i 90  pm2.21ni 92  mt3 99  nsyl2 103  nsyl4 105  pm3.26im 120  pm3.27im 121  bicon1i 193  hbnt 710  eq4ds 823  1st2val 3097  eceqopreq 3249  mapprc 3260  map0b 3267  pw2en 3348  unbndrank 3527  str 5698

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

metamath.org