Theorem con4i 130

Description: Inference rule derived from axiom ax-3 8. (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  1807  ax6fromc10  2213  axc711to11  2233  axc5c711to11  2237  necon2aiOLD  2696  elimasni  5355  ndmfvrcl  5882  brabv  6317  oprssdm  6431  ndmovrcl  6436  omelon2  6683  omopthi  7296  fsuppres  7843  sdomsdomcardi  8341  alephgeom  8452  pwcdadom  8585  rankcf  9144  adderpq  9323  mulerpq  9324  ltadd2i  9704  ssnn0fi  12050  sadcp1  13953  setcepi  15262  oduclatb  15620  cntzrcl  16153  pmtrfrn  16272  dprddomcld  16816  dprdsubg  16854  mplrcl  17918  psrbagsn  17924  dsmmbas2  18528  dsmmfi  18529  istps  19197  bwthOLD  19670  isusp  20492  dscmet  20821  dscopn  20822  i1f1lem  21824  sqff1o  23177  umgrafi  23985  usgraedgrnv  24039  nbgranself2  24098  wwlknndef  24399  clwwlknndef  24435  dmadjrnb  26487  axpowprim  28537  opelco3  28771  sltintdifex  28986  pw2f1ocnv  30572  kelac1  30602  axc5c4c711toc5  30842  axc5c4c711to11  30845  afvvdm  31648  afvvfunressn  31650  afvvv  31652  afvfv0bi  31659