Theorem a3i 77

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 80  notnot1 89  con1iOLD 101  con2iOLD 103  ax67to7 1063  ax467to7 1067  modal-b 1069  necon4ai 1671  vtoclibr 3270  unixp0 3575  ndmfvrcl 3803  oprssdm 4100  ndmoprrcl 4104  ecelqsdm 4360  sdomex 4536  infeq5 4683  sdomsdomcard 4913  alephgeom 4947  ltadd2i 5655  ltmul1ii 5879  discrlem3 6748  efltbi 7498  tpsex 7696  issubg 8200  vcex 8283  nvex 8314  cosh111lem2 8798  dmadjrnb 9913  irredi 10405

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

Copyright terms: Public domain