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  1849  ax6fromc10  2213  axc711to11  2233  axc5c711to11  2237  necon2aiOLD  2679  elimasni  5354  ndmfvrcl  5881  brabv  6327  oprssdm  6441  ndmovrcl  6446  omelon2  6697  omopthi  7308  fsuppres  7856  sdomsdomcardi  8355  alephgeom  8466  pwcdadom  8599  rankcf  9158  adderpq  9337  mulerpq  9338  ltadd2iOLD  9719  ssnn0fi  12073  sadcp1  13982  setcepi  15289  oduclatb  15648  cntzrcl  16239  pmtrfrn  16357  dprddomcld  16906  dprdsubg  16945  psrbagsn  18034  dsmmbas2  18641  dsmmfi  18642  istps  19310  bwthOLD  19784  isusp  20637  dscmet  20966  dscopn  20967  i1f1lem  21969  sqff1o  23328  umgrafi  24194  usgraedgrnv  24249  nbgranself2  24308  wwlknndef  24609  clwwlknndef  24645  dmadjrnb  26697  axpowprim  28949  opelco3  29183  sltintdifex  29398  pw2f1ocnv  30954  kelac1  30984  axc5c4c711toc5  31263  axc5c4c711to11  31266  afvvdm  32064  afvvfunressn  32066  afvvv  32068  afvfv0bi  32075