Theorem con3i 155

Description: A contraposition inference. Inference associated with con3 154. Its associated inference is mto 200. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)

Hypothesis

Ref	Expression
con3i.a	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
con3i	⊢ (¬ 𝜓 → ¬ 𝜑)

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con3i.a	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl 141	1 ⊢ (¬ 𝜓 → ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  conax1  171  pm2.65iOLD  197  pm5.21ni  380  pm2.45  895  pm2.46  896  con3ALT  1101  rb-ax2  1786  rb-ax4  1788  emptyex  1942  excomimw  2079  naev  2097  ax13ALT  2457  barocoALT  2704  necon3bi  2985  prcnel  3479  sbc2or  3751  nel1nelin  4107  nel2nelin  4108  difrab  4266  sbcel12  4372  sbcne12  4376  sbcel2  4379  rexn0  4455  ifeqor  4537  ifan  4539  nelpri  4617  nelprd  4619  eqoreldif  4647  vneqv  5276  snexALT  5352  csbopab  5537  nprrel12  5716  csbxp  5760  soirri  6138  frinf  6316  predpoirr  6362  predfrirr  6363  nsuceq0  6474  csbiota  6559  eldifpw  7814  nlimsucg  7887  tfindsg  7906  findsg  7943  curry1val  8153  curry2val  8157  fsetdmprc0  8915  fiprc  9110  sdomirr  9171  domtriord  9180  2pwuninel  9189  mapdom1  9199  nfielex  9303  relprcnfsupp  9394  wemapso2  9584  card2inf  9586  en2lp  9644  wemapwe  9735  rankxplim3  9935  fidomtri2  10114  alephnbtwn  10189  kmlem2  10269  isfin7-2  10513  dominf  10562  ac6n  10602  alephval2  10696  dominfac  10697  gchdomtri  10753  nlt1pi  11030  indval0  12364  zeo  12825  bcpasc  14506  hashnemnf  14529  hasheq0  14548  hashunx  14571  hashbc  14639  pfxval0  14868  flodddiv4lt  16631  prmreclem4  17141  ressinbas  17467  natfval  18174  fucbas  18188  fuchom  18189  coafval  18289  efgval  19982  gsum2dlem1  20235  gsum2dlem2  20236  dprddomprc  20267  dprdval0prc  20269  isfieldidl  21591  psrvscafval  22311  mavmul0g  22923  mdetralt  22978  mdetunilem9  22990  matunitlindflem1  23049  cfinfil  24267  pcofval  25386  i1fima2  26055  i1fd  26057  itgeq2  26153  ibladdlem  26195  nbgrnself2  29998  clwwlknondisj  30759  nfrgr2v  30930  avril1  31121  nmobndseqi  31438  nonbooli  32310  chpssati  33022  nn0difffzod  33492  hashxpe  33495  gsumfs2d  33721  1arithufdlem4  34183  hasheuni  34828  ddemeas  34980  bnj1143  35531  rmo6  35821  erscottd  35884  fineqvnttrclse  35933  fineqvinfep  35934  kardval  35961  kard0b  35968  distel  36780  linedegen  37123  ordcmp  37450  bj-babygodel  37688  bj-nexrt  37809  bj-csbprc  38037  onsucuni3  38558  finxpnom  38592  wl-ifp-ncond1  38655  unccur  38794  poimirlem26  38832  poimirlem27  38833  poimirlem31  38837  cnambfre  38854  ibladdnclem  38862  tsbi3  39333  mopickr  39569  ax13fromc9  40229  axc711  40237  axc711toc7  40239  axc5c711toc7  40243  equidqe  40245  equidq  40247  ax12indalem  40268  hdmap1eulem  43145  hdmapevec  43158  intnanrt  43524  jm2.22  44268  clsk1indlem2  45303  nanorxor  45550  binomcxplemfrat  45596  binomcxplemradcnv  45597  pm10.251  45605  axc5c4c711toc7  45649  en3lpVD  46087  ax6e2ndeqVD  46151  2sb5ndVD  46152  ax6e2ndeqALT  46173  2sb5ndALT  46174  sineq0ALT  46179  axccdom  46508  fzdifsuc2  46599  liminf0  47076  cncfiooicc  47177  itgcoscmulx  47252  sge0sn  47662  isomenndlem  47813  hoidmvlelem2  47879  et-ltneverrefl  48154  quantgodelALT  48158  nabctnabc  48274  dfafv2  48475  afv2ndefb  48567  spr0el  48837  prmdvdsfmtnof1lem2  48943  fucofvalne  50778