Theorem a3i 69

Description: Inference rule derived from axiom ax-3 5.

Hypothesis

Ref	Expression
a3i.1	⊢ (¬ φ → ¬ ψ)

Assertion

Ref	Expression
a3i	⊢ (ψ → φ)

Proof of Theorem a3i

Step	Hyp	Ref	Expression
1		a3i.1	. 2 ⊢ (¬ φ → ¬ ψ)
2		ax-3 5	. 2 ⊢ ((¬ φ → ¬ ψ) → (ψ → φ))
3	1, 2	ax-mp 6	1 ⊢ (ψ → φ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  pm2.21i 73  negb 79  con1i 88  con2i 89  ax9a 808  vtoclibr 2451  ndmfvrcl 2849  oprssdm 3056  ndmoprrcl 3060  ecelqsdm 3235  map0 3268  sdomex 3315  inf5 3472  rankr1 3518  scott0 3542  sdomsdomcard 3654  alephgeom 3687  discrlem3 4715

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

metamath.org