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  1798  ax6fromc10  2198  axc711to11  2218  axc5c711to11  2222  necon2ai  2654  elimasni  5194  ndmfvrcl  5713  brabv  6130  oprssdm  6242  ndmovrcl  6247  omelon2  6486  omopthi  7094  fsuppres  7643  sdomsdomcardi  8139  alephgeom  8250  pwcdadom  8383  rankcf  8942  adderpq  9123  mulerpq  9124  ltadd2i  9503  sadcp1  13649  setcepi  14954  oduclatb  15312  cntzrcl  15843  pmtrfrn  15962  dprddomcld  16481  dprdsubg  16519  mplrcl  17569  psrbagsn  17575  strov2rcl  17690  dsmmbas2  18160  dsmmfi  18161  istps  18539  bwthOLD  19012  isusp  19834  dscmet  20163  dscopn  20164  i1f1lem  21165  sqff1o  22518  umgrafi  23254  usgraedgrnv  23294  nbgranself2  23345  dmadjrnb  25308  axpowprim  27353  opelco3  27587  sltintdifex  27802  pw2f1ocnv  29383  kelac1  29413  axc5c4c711toc5  29653  axc5c4c711to11  29656  afvvdm  30044  afvvfunressn  30046  afvvv  30048  afvfv0bi  30055  wwlknndef  30366  clwwlknndef  30433  ssnn0fi  30743