Theorem a3i 74

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

Hypothesis

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

Assertion

Ref	Expression
a3i	⊢ (ψ → φ)

Proof of Theorem a3i

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

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  pm2.21i 77  negb 86  con1i 96  con2i 97  ax67to7 1020  ax467to7 1024  modal-b 1026  necon4ai 1621  vtoclibr 3208  unixp0 3510  ndmfvrcl 3737  oprssdm 4033  ndmoprrcl 4038  ecelqsdm 4289  sdomex 4459  infeq5 4601  sdomsdomcard 4828  alephgeom 4862  ltadd2 5572  ltmul1i 5785  discrlem3 6596  efltb 7356  tpsex 7555  issubg 8068  vcex 8151  nvex 8182  cosh111lem2 8649  dmadjrnb 9770  irred 10258

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

Copyright terms: Public domain