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  nbior  856  pm5.14  881  con3th  949  cadanOLD  1434  rb-ax2  1560  rb-ax4  1562  thema1a  1579  ax13  1995  sbequi  2066  sbnOLD  2083  ax13fromc9  2206  axc711  2215  axc711toc7  2217  axc5c711toc7  2221  equidqe  2223  equidq  2225  ax12indalem  2246  euor2  2312  euor2OLD  2313  moexexOLD  2350  baroco  2393  necon1bi  2659  eueq3  3139  sbc2or  3200  sbcimdv  3260  sbcrext  3274  difrab  3629  abvor0  3660  csbprc  3678  sbcel12  3680  sbcne12  3684  sbcel2  3688  ifeqor  3838  ifan  3840  nelpri  3903  nelprd  3904  opprc1  4087  opprc2  4088  sbcbr123  4348  snexALT  4483  mosubopt  4594  csbopab  4625  csbxp  4923  soirri  5229  soirriOLD  5234  csbiota  5415  nfvres  5725  fvco4i  5774  fvmptex  5789  fvopab4ndm  5799  ressnop0  5894  csbriota  6069  ovprc  6123  ovprc1  6124  ovprc2  6125  ndmovass  6256  ndmovdistr  6257  eldifpw  6393  nlimsucg  6458  tfindsg  6476  findsg  6508  curry1val  6670  curry2val  6674  extmptsuppeq  6718  funsssuppss  6720  eceqoveq  7210  fiprc  7396  sdomirr  7453  domtriord  7462  2pwuninel  7471  mapdom1  7481  nfielex  7546  relprcnfsupp  7628  supval2  7710  wemapso2  7773  card2inf  7775  en2lp  7824  wemapwe  7933  wemapweOLD  7934  rankxplim3  8093  fidomtri2  8169  alephnbtwn  8246  kmlem2  8325  isfin7-2  8570  dominf  8619  ac6n  8659  alephval2  8741  dominfac  8742  axpowndlem3  8769  gchdomtri  8801  nlt1pi  9080  adderpq  9130  mulerpq  9131  zeo  10732  fzoval  11559  bcpasc  12102  hashnemnf  12120  hasheq0  12136  hashunx  12154  hashbc  12211  prmreclem4  13985  ressinbas  14239  natfval  14861  fucbas  14875  fuchom  14876  homarcl  14901  arwval  14916  coafval  14937  grpidval  15437  symgbas  15890  efgval  16219  gsum2dlem1  16466  gsum2dlem2  16467  gsum2dOLD  16469  dprddomprc  16487  dprdval0prc  16489  psrvscafval  17466  mavmul0g  18369  mdetralt  18419  mdetunilem9  18431  tgdif0  18602  resstopn  18795  cfinfil  19471  pcofval  20587  i1fima2  21162  i1fd  21164  itgeq2  21260  ibladdlem  21302  cusgrafi  23395  uvtx01vtx  23405  avril1  23661  nmobndseqi  24184  nonbooli  25059  chpssati  25772  xrge0neqmnf  26157  hasheuni  26539  ddemeas  26657  rdgprc0  27612  distel  27622  predpoirr  27663  predfrirr  27664  linedegen  28179  ordcmp  28298  wl-naev  28363  wl-ax11-lem8  28413  cnambfre  28445  itg2addnclem3  28450  ibladdnclem  28453  frinfm  28634  tsbi3  28951  jm2.22  29349  pm10.251  29617  axc5c4c711toc7  29663  infrglb  29776  ndmafv  30051  nfunsnafv  30053  afvprc  30055  afvnufveq  30058  aovprc  30099  ndmaovass  30117  ndmaovdistr  30118  frgra2v  30596  2spotiundisj  30660  numclwwlkdisj  30678  en3lpVD  31586  ax6e2ndeqVD  31650  2sb5ndVD  31651  ax6e2ndeqALT  31672  2sb5ndALT  31673  sineq0ALT  31678  bnj1143  31789  bj-con3ALT  32103  bj-babygodel  32128  bj-nexrt  32186  bj-csbprc  32416  bj-projval  32494  hdmap1eulem  35474  hdmapevec  35488