Theorem con4i 130

Description: Inference rule derived from axiom ax-3 8. Its associated inference is mt4 137. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 21-Jun-2013.)

Hypothesis

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

Assertion

Ref	Expression
con4i	|- ( ps -> ph )

Proof of Theorem con4i

Step	Hyp	Ref	Expression
1		notnot1 122	. 2 |- ( ps -> -. -. ps )
2		con4i.1	. 2 |- ( -. ph -> -. ps )
3	1, 2	nsyl2 127	1 |- ( ps -> ph )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.21i  131  mt4  137  modal-b  1871  necon2aiOLD  2618  elimasni  5276  ndmfvrcl  5799  brabv  6241  oprssdm  6355  ndmovrcl  6360  omelon2  6611  omopthi  7224  fsuppres  7769  sdomsdomcardi  8265  alephgeom  8376  pwcdadom  8509  rankcf  9066  adderpq  9245  mulerpq  9246  ltadd2iOLD  9627  ssnn0fi  11997  sadcp1  14107  setcepi  15484  oduclatb  15891  cntzrcl  16482  pmtrfrn  16600  dprddomcld  17145  dprdsubg  17184  psrbagsn  18273  dsmmbas2  18859  dsmmfi  18860  istps  19522  isusp  20849  dscmet  21178  dscopn  21179  i1f1lem  22181  sqff1o  23573  umgrafi  24443  usgraedgrnv  24498  nbgranself2  24557  wwlknndef  24858  clwwlknndef  24894  dmadjrnb  26941  axpowprim  29242  opelco3  29373  sltintdifex  29588  pw2f1ocnv  31145  kelac1  31175  axc5c4c711toc5  31477  axc5c4c711to11  31480  afvvdm  32392  afvvfunressn  32394  afvvv  32396  afvfv0bi  32403  ax6fromc10  35040  axc711to11  35060  axc5c711to11  35064