Theorem con4i 133

Description: Inference associated with ax-3 8. Its associated inference is mt4 142. (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 125	. 2 |- ( ps -> -. -. ps )
2		con4i.1	. 2 |- ( -. ph -> -. ps )
3	1, 2	nsyl2 130	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  134  mt4  142  modal-b  1916  necon2aiOLD  2667  elimasni  5215  ndmfvrcl  5906  brabv  6350  oprssdm  6464  ndmovrcl  6469  omelon2  6718  omopthi  7366  fsuppres  7914  sdomsdomcardi  8404  alephgeom  8511  pwcdadom  8644  rankcf  9201  adderpq  9380  mulerpq  9381  ltadd2iOLD  9765  ssnn0fi  12194  sadcp1  14403  setcepi  15934  oduclatb  16341  cntzrcl  16932  pmtrfrn  17050  dprddomcld  17568  dprdsubg  17592  psrbagsn  18653  dsmmbas2  19231  dsmmfi  19232  istps  19882  isusp  21207  dscmet  21518  dscopn  21519  i1f1lem  22524  sqff1o  23972  umgrafi  24895  usgraedgrnv  24950  nbgranself2  25009  wwlknndef  25310  clwwlknndef  25346  dmadjrnb  27394  axpowprim  30119  opelco3  30207  sltintdifex  30337  topdifinffinlem  31484  ax6fromc10  32176  axc711to11  32196  axc5c711to11  32200  pw2f1ocnv  35597  kelac1  35626  axc5c4c711toc5  36389  axc5c4c711to11  36392  disjrnmpt2  37085  afvvdm  38032  afvvfunressn  38034  afvvv  38036  afvfv0bi  38043