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 1018  ax467to7 1022  modal-b 1024  necon4ai 1616  vtoclibr 3203  unixp0 3504  ndmfvrcl 3731  oprssdm 4027  ndmoprrcl 4032  ecelqsdm 4283  sdomex 4453  infeq5 4593  sdomsdomcard 4820  alephgeom 4854  ltadd2 5564  ltmul1i 5777  discrlem3 6588  efltb 7348  tpsex 7547  issubg 8053  vcex 8137  nvex 8169  cosh111lem2 8630  dmadjrnb 9747  irred 10229

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

Copyright terms: Public domain