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  rb-ax2  1571  rb-ax4  1573  stoic1a  1590  ax13  2031  sbequi  2100  ax13fromc9  2219  axc711  2228  axc711toc7  2230  axc5c711toc7  2234  equidqe  2236  equidq  2238  ax12indalem  2259  euor2  2317  baroco  2389  necon3bi  2670  necon1biOLD  2675  eueq3  3258  sbc2or  3320  sbcimdv  3380  sbcrext  3394  difrab  3754  abvor0  3785  csbprc  3803  sbcel12  3805  sbcne12  3809  sbcel2  3813  ifeqor  3966  ifan  3968  nelpri  4031  nelprd  4032  opprc1  4221  opprc2  4222  sbcbr123  4484  snexALT  4619  mosubopt  4731  csbopab  4765  csbxp  5067  soirri  5379  soirriOLD  5384  csbiota  5566  nfvres  5882  fvco4i  5932  fvmptex  5947  fvopab4ndm  5959  ressnop0  6059  csbriota  6250  ovprc  6307  ovprc1  6308  ovprc2  6309  ndmovass  6444  ndmovdistr  6445  eldifpw  6593  nlimsucg  6658  tfindsg  6676  findsg  6708  curry1val  6874  curry2val  6878  extmptsuppeq  6922  funsssuppss  6924  eceqoveq  7414  fiprc  7595  sdomirr  7652  domtriord  7661  2pwuninel  7670  mapdom1  7680  nfielex  7746  relprcnfsupp  7830  supval2  7913  wemapso2  7977  card2inf  7979  en2lp  8028  wemapwe  8137  wemapweOLD  8138  rankxplim3  8297  fidomtri2  8373  alephnbtwn  8450  kmlem2  8529  isfin7-2  8774  dominf  8823  ac6n  8863  alephval2  8945  dominfac  8946  axpowndlem3  8973  gchdomtri  9005  nlt1pi  9282  adderpq  9332  mulerpq  9333  zeo  10949  fzoval  11804  bcpasc  12373  hashnemnf  12391  hasheq0  12407  hashunx  12428  hashbc  12476  prmreclem4  14309  ressinbas  14565  natfval  15184  fucbas  15198  fuchom  15199  homarcl  15224  arwval  15239  coafval  15260  grpidval  15756  symgbas  16274  efgval  16604  gsum2dlem1  16866  gsum2dlem2  16867  gsum2dOLD  16869  dprddomprc  16900  dprdval0prc  16902  psrvscafval  17911  mavmul0g  18922  mdetralt  18977  mdetunilem9  18989  tgdif0  19360  resstopn  19553  cfinfil  20260  pcofval  21376  i1fima2  21952  i1fd  21954  itgeq2  22050  ibladdlem  22092  cusgrafi  24347  uvtx01vtx  24357  frgra2v  24864  2spotiundisj  24927  numclwwlkdisj  24945  avril1  25036  nmobndseqi  25559  nonbooli  26434  chpssati  27147  xrge0neqmnf  27545  hasheuni  27957  ddemeas  28074  rdgprc0  29194  distel  29204  predpoirr  29245  predfrirr  29246  linedegen  29761  ordcmp  29880  wl-naev  29950  wl-ax11-lem8  30000  cnambfre  30031  itg2addnclem3  30036  ibladdnclem  30039  frinfm  30194  tsbi3  30510  jm2.22  30905  nanorxor  31154  pm10.251  31212  axc5c4c711toc7  31258  infrglb  31508  cncfiooicc  31600  itgcoscmulx  31654  ndmafv  32059  nfunsnafv  32061  afvprc  32063  afvnufveq  32066  aovprc  32107  ndmaovass  32125  ndmaovdistr  32126  en3lpVD  33353  ax6e2ndeqVD  33417  2sb5ndVD  33418  ax6e2ndeqALT  33439  2sb5ndALT  33440  sineq0ALT  33445  bnj1143  33556  bj-con3ALT  33875  bj-babygodel  33905  bj-nexrt  33959  bj-csbprc  34188  bj-projval  34266  hdmap1eulem  37253  hdmapevec  37267  rp-fakeimass  37401