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 1024  ax467to7 1028  modal-b 1030  necon4ai 1627  vtoclibr 3219  unixp0 3524  ndmfvrcl 3752  oprssdm 4048  ndmoprrcl 4052  ecelqsdm 4305  sdomex 4479  infeq5 4630  sdomsdomcard 4859  alephgeom 4893  ltadd2 5602  ltmul1i 5823  discrlem3 6659  efltb 7407  tpsex 7606  issubg 8112  vcex 8195  nvex 8226  cosh111lem2 8710  dmadjrnb 9825  irred 10316

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

Copyright terms: Public domain