Theorem con3i 135

Description: A contraposition inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)

Hypothesis

Ref	Expression
con3i.a	|- ( ph -> ps )

Assertion

Ref	Expression
con3i	|- ( -. ps -> -. ph )

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( -. ps -> -. ps )
2		con3i.a	. 2 |- ( ph -> ps )
3	1, 2	nsyl 121	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.51  153  pm2.65i  173  pm5.21ni  352  pm2.45  397  pm2.46  398  nbiorOLD  859  pm5.14  884  con3th  956  cadanOLD  1444  rb-ax2  1570  rb-ax4  1572  thema1a  1589  ax13  2020  sbequi  2089  sbnOLD  2106  ax13fromc9  2228  axc711  2237  axc711toc7  2239  axc5c711toc7  2243  equidqe  2245  equidq  2247  ax12indalem  2268  euor2  2334  euor2OLD  2335  moexexOLD  2372  baroco  2415  necon3bi  2696  necon1biOLD  2701  eueq3  3278  sbc2or  3340  sbcimdv  3400  sbcrext  3414  difrab  3772  abvor0  3803  csbprc  3821  sbcel12  3823  sbcne12  3827  sbcel2  3831  ifeqor  3983  ifan  3985  nelpri  4048  nelprd  4049  opprc1  4236  opprc2  4237  sbcbr123  4498  snexALT  4633  mosubopt  4745  csbopab  4779  csbxp  5079  soirri  5391  soirriOLD  5396  csbiota  5578  nfvres  5894  fvco4i  5943  fvmptex  5958  fvopab4ndm  5970  ressnop0  6066  csbriota  6255  ovprc  6309  ovprc1  6310  ovprc2  6311  ndmovass  6445  ndmovdistr  6446  eldifpw  6590  nlimsucg  6655  tfindsg  6673  findsg  6705  curry1val  6873  curry2val  6877  extmptsuppeq  6921  funsssuppss  6923  eceqoveq  7413  fiprc  7594  sdomirr  7651  domtriord  7660  2pwuninel  7669  mapdom1  7679  nfielex  7745  relprcnfsupp  7828  supval2  7911  wemapso2  7975  card2inf  7977  en2lp  8026  wemapwe  8135  wemapweOLD  8136  rankxplim3  8295  fidomtri2  8371  alephnbtwn  8448  kmlem2  8527  isfin7-2  8772  dominf  8821  ac6n  8861  alephval2  8943  dominfac  8944  axpowndlem3  8971  gchdomtri  9003  nlt1pi  9280  adderpq  9330  mulerpq  9331  zeo  10942  fzoval  11794  bcpasc  12363  hashnemnf  12381  hasheq0  12397  hashunx  12418  hashbc  12464  prmreclem4  14292  ressinbas  14547  natfval  15169  fucbas  15183  fuchom  15184  homarcl  15209  arwval  15224  coafval  15245  grpidval  15745  symgbas  16200  efgval  16531  gsum2dlem1  16788  gsum2dlem2  16789  gsum2dOLD  16791  dprddomprc  16822  dprdval0prc  16824  psrvscafval  17814  mavmul0g  18822  mdetralt  18877  mdetunilem9  18889  tgdif0  19260  resstopn  19453  cfinfil  20129  pcofval  21245  i1fima2  21821  i1fd  21823  itgeq2  21919  ibladdlem  21961  cusgrafi  24158  uvtx01vtx  24168  frgra2v  24675  2spotiundisj  24739  numclwwlkdisj  24757  avril1  24847  nmobndseqi  25370  nonbooli  26245  chpssati  26958  xrge0neqmnf  27341  hasheuni  27731  ddemeas  27848  rdgprc0  28803  distel  28813  predpoirr  28854  predfrirr  28855  linedegen  29370  ordcmp  29489  wl-naev  29559  wl-ax11-lem8  29609  cnambfre  29640  itg2addnclem3  29645  ibladdnclem  29648  frinfm  29829  tsbi3  30146  jm2.22  30541  pm10.251  30843  axc5c4c711toc7  30889  infrglb  31140  sumnnodd  31172  icccncfext  31226  cncfiooicc  31233  itgcoscmulx  31287  fourierdlem104  31511  ndmafv  31692  nfunsnafv  31694  afvprc  31696  afvnufveq  31699  aovprc  31740  ndmaovass  31758  ndmaovdistr  31759  en3lpVD  32725  ax6e2ndeqVD  32789  2sb5ndVD  32790  ax6e2ndeqALT  32811  2sb5ndALT  32812  sineq0ALT  32817  bnj1143  32928  bj-con3ALT  33242  bj-babygodel  33273  bj-nexrt  33327  bj-csbprc  33557  bj-projval  33635  hdmap1eulem  36621  hdmapevec  36635