Theorem con3i 142

Description: A contraposition inference. Inference associated with con3 141. Its associated inference is mto 181. (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 126	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  158  pm2.65i  178  pm5.21ni  358  pm2.45  403  pm2.46  404  nbiorOLD  877  pm5.14  902  con3th  975  rb-ax2  1646  rb-ax4  1648  stoic1aOLD  1666  ax13  2151  sbequi  2214  euor2  2353  baroco  2411  necon3bi  2661  prcnel  3071  eueq3  3224  sbc2or  3287  sbcimdv  3340  sbcrext  3352  difrab  3728  abvor0  3761  csbprc  3781  sbcel12  3783  sbcne12  3786  sbcel2  3789  ifeqor  3936  ifan  3938  nelpri  3999  nelprd  4000  opprc1  4202  opprc2  4203  sbcbr123  4467  snexALT  4602  mosubopt  4712  csbopab  4746  csbxp  4934  soirri  5244  predpoirr  5426  predfrirr  5427  csbiota  5593  nfvres  5917  fvco4i  5965  fvmptex  5982  fvopab4ndm  5994  ressnop0  6094  csbriota  6288  ovprc  6344  ovprc1  6345  ovprc2  6346  ndmovass  6483  ndmovdistr  6484  eldifpw  6629  nlimsucg  6695  tfindsg  6713  findsg  6746  curry1val  6915  curry2val  6919  extmptsuppeq  6965  funsssuppss  6967  eceqoveq  7493  fiprc  7676  sdomirr  7734  domtriord  7743  2pwuninel  7752  mapdom1  7762  nfielex  7825  relprcnfsupp  7911  supval2  7994  wemapso2  8093  card2inf  8095  en2lp  8143  wemapwe  8227  rankxplim3  8377  fidomtri2  8453  alephnbtwn  8527  kmlem2  8606  isfin7-2  8851  dominf  8900  ac6n  8940  alephval2  9022  dominfac  9023  axpowndlem3  9049  gchdomtri  9079  nlt1pi  9356  adderpq  9406  mulerpq  9407  zeo  11049  xrge0neqmnf  11765  fzoval  11951  bcpasc  12537  hashnemnf  12558  hasheq0  12575  hashunx  12596  hashbc  12648  prmreclem4  14911  ressinbas  15233  natfval  15899  fucbas  15913  fuchom  15914  homarcl  15971  arwval  15986  coafval  16007  grpidval  16551  symgbas  17069  efgval  17415  gsum2dlem1  17650  gsum2dlem2  17651  dprddomprc  17680  dprdval0prc  17682  psrvscafval  18662  mavmul0g  19626  mdetralt  19681  mdetunilem9  19693  tgdif0  20056  resstopn  20250  cfinfil  20956  pcofval  22089  i1fima2  22685  i1fd  22687  itgeq2  22783  ibladdlem  22825  cusgrafi  25258  uvtx01vtx  25268  frgra2v  25775  2spotiundisj  25838  numclwwlkdisj  25856  avril1  25948  nmobndseqi  26468  nonbooli  27352  chpssati  28064  hasheuni  28954  inelpisys  29024  ddemeas  29107  bnj1143  29650  rdgprc0  30488  distel  30498  linedegen  30958  ordcmp  31155  bj-con3thALT  31199  bj-babygodel  31231  bj-nexrt  31329  bj-csbprc  31555  bj-projval  31634  onsucuni3  31814  finxpnom  31837  wl-naev  31906  wl-ax11-lem8  31966  poimirlem26  32010  poimirlem27  32011  poimirlem31  32015  cnambfre  32033  itg2addnclem3  32039  ibladdnclem  32042  frinfm  32106  tsbi3  32421  ax13fromc9  32520  axc711  32529  axc711toc7  32531  axc5c711toc7  32535  equidqe  32537  equidq  32539  ax12indalem  32560  hdmap1eulem  35436  hdmapevec  35450  jm2.22  35894  rp-fakeimass  36200  nanorxor  36696  binomcxplemfrat  36743  binomcxplemradcnv  36744  pm10.251  36752  axc5c4c711toc7  36798  en3lpVD  37280  ax6e2ndeqVD  37345  2sb5ndVD  37346  ax6e2ndeqALT  37367  2sb5ndALT  37368  sineq0ALT  37373  fzdifsuc2  37567  infrglbOLD  37706  cncfiooicc  37809  itgcoscmulx  37883  sge0sn  38258  iundjiunlem  38334  isomenndlem  38388  hoidmvlelem2  38455  nabctnabc  38556  ndmafv  38679  nfunsnafv  38681  afvprc  38683  afvnufveq  38686  aovprc  38727  ndmaovass  38745  ndmaovdistr  38746  fundmge2nop  39067  fun2dmnop  39068