Theorem con4i 135

Description: Inference associated with con4 107. Its associated inference is mt4 144. (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 126	. 2 |- ( ps -> -. -. ps )
2		con4i.1	. 2 |- ( -. ph -> -. ps )
3	1, 2	nsyl2 132	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  136  mt4  144  modal-b  1961  elimasni  5201  ndmfvrcl  5904  brabv  6354  oprssdm  6469  ndmovrcl  6474  omelon2  6723  omopthi  7376  fsuppres  7926  sdomsdomcardi  8423  alephgeom  8531  pwcdadom  8664  rankcf  9220  adderpq  9399  mulerpq  9400  ssnn0fi  12235  sadcp1  14508  setcepi  16061  oduclatb  16468  cntzrcl  17059  pmtrfrn  17177  dprddomcld  17711  dprdsubg  17735  psrbagsn  18795  dsmmbas2  19377  dsmmfi  19378  istps  20028  isusp  21354  dscmet  21665  dscopn  21666  i1f1lem  22726  sqff1o  24188  umgrafi  25128  usgraedgrnv  25183  nbgranself2  25243  wwlknndef  25544  clwwlknndef  25580  dmadjrnb  27640  axpowprim  30403  opelco3  30491  sltintdifex  30621  bj-modal5e  31313  bj-modal4e  31374  topdifinffinlem  31820  finxp1o  31854  ax6fromc10  32532  axc711to11  32552  axc5c711to11  32556  pw2f1ocnv  35963  kelac1  35992  relintabex  36258  axc5c4c711toc5  36823  axc5c4c711to11  36826  disjrnmpt2  37534  afvvdm  38788  afvvfunressn  38790  afvvv  38792  afvfv0bi  38799  upgrfi  39337