Theorem a3i 74

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

Hypothesis

Ref	Expression
a3i.1	|- (-. ph -> -. ps)

Assertion

Ref	Expression
a3i	|- (ps -> ph)

Proof of Theorem a3i

Step	Hyp	Ref	Expression
1		a3i.1	. 2 |- (-. ph -> -. ps)
2		ax-3 6	. 2 |- ((-. ph -> -. ps) -> (ps -> ph))
3	1, 2	ax-mp 7	1 |- (ps -> ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.21i 77  negb 86  con1i 96  con2i 97  ax67to7 996  ax467to7 1000  modal-b 1004  necon4ai 1600  vtoclibr 3175  unixp0 3459  ndmfvrcl 3685  oprssdm 3981  ndmoprrcl 3986  ecelqsdm 4237  sdomex 4407  infeq5 4545  sdomsdomcard 4771  alephgeom 4805  ltadd2 5515  ltmul1i 5728  discrlem3 6539  efltb 7299  tpsex 7498  issubg 8001  cosh111lem2 8543  dmadjrnb 9961  irred 10443

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

Copyright terms: Public domain