Theorem con4i 90

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

Hypothesis

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

Assertion

Ref	Expression
con4i	|- (ps -> ph)

Proof of Theorem con4i

Step	Hyp	Ref	Expression
1		con4i.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 93  notnot1 102  ax67to7 1369  ax467to7 1373  modal-b 1375  necon2ai 2051  necon4aiOLD 2068  vtoclibr 4035  elimasni 4292  unixp0 4423  ndmfvrcl 4703  oprssdm 4975  ndmoprrcl 4979  ecelqsdm 5358  sdomex 5536  riotaclb 5573  infeq5 5727  sdomsdomcard 6000  alephgeom 6030  ltadd2i 6765  ltmul1ii 6999  discrlem3 7908  efltbi 8672  tpsex 8874  issubg 9425  vcex 9531  nvex 9562  cosh111lem2 10069  dmadjrnb 11467  irredi 11966  axpowprim 13788  sltintdifex 14004  evpexun 14322  dstr 14516  bwt2 14960  ax4567to4 16360  ax4567to7 16363

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

Copyright terms: Public domain