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  1940  excomimw  2077  naev  2095  ax13ALT  2454  barocoALT  2701  necon3bi  2981  prcnel  3475  sbc2or  3748  nel1nelin  4153  nel2nelin  4154  difrab  4264  sbcel12  4369  sbcne12  4373  sbcel2  4376  rexn0  4452  ifeqor  4534  ifan  4536  nelpri  4616  nelprd  4618  eqoreldif  4646  vneqv  5273  snexALT  5348  csbopab  5534  nprrel12  5713  csbxp  5756  soirri  6120  predpoirr  6331  predfrirr  6332  nsuceq0  6443  csbiota  6526  eldifpw  7767  nlimsucg  7838  tfindsg  7857  findsg  7894  curry1val  8102  curry2val  8106  fsetdmprc0  8856  fiprc  9051  sdomirr  9112  domtriord  9121  2pwuninel  9130  mapdom1  9140  nfielex  9244  relprcnfsupp  9334  wemapso2  9525  card2inf  9527  en2lp  9585  wemapwe  9676  rankxplim3  9863  fidomtri2  9999  alephnbtwn  10074  kmlem2  10154  isfin7-2  10398  dominf  10447  ac6n  10487  alephval2  10581  dominfac  10582  gchdomtri  10638  nlt1pi  10915  indval0  12246  zeo  12707  bcpasc  14385  hashnemnf  14408  hasheq0  14427  hashunx  14450  hashbc  14518  pfxval0  14746  flodddiv4lt  16507  prmreclem4  17011  ressinbas  17337  natfval  18038  fucbas  18052  fuchom  18053  coafval  18153  efgval  19844  gsum2dlem1  20097  gsum2dlem2  20098  dprddomprc  20129  dprdval0prc  20131  isfieldidl  21449  psrvscafval  22163  mavmul0g  22775  mdetralt  22830  mdetunilem9  22842  matunitlindflem1  22901  cfinfil  24119  pcofval  25238  i1fima2  25907  i1fd  25909  itgeq2  26005  ibladdlem  26047  nbgrnself2  29820  clwwlknondisj  30581  nfrgr2v  30752  avril1  30943  nmobndseqi  31260  nonbooli  32132  chpssati  32844  nn0difffzod  33275  hashxpe  33278  gsumfs2d  33501  1arithufdlem4  33957  hasheuni  34595  ddemeas  34747  bnj1143  35299  fineqvnttrclse  35650  fineqvinfep  35651  kardval  35678  kard0b  35685  distel  36380  linedegen  36723  ordcmp  37066  bj-babygodel  37304  bj-nexrt  37425  bj-csbprc  37653  onsucuni3  38121  finxpnom  38155  wl-ifp-ncond1  38218  unccur  38357  poimirlem26  38395  poimirlem27  38396  poimirlem31  38400  cnambfre  38417  ibladdnclem  38425  frinfm  38485  tsbi3  38883  mopickr  39119  ax13fromc9  39779  axc711  39787  axc711toc7  39789  axc5c711toc7  39793  equidqe  39795  equidq  39797  ax12indalem  39818  hdmap1eulem  42695  hdmapevec  42708  intnanrt  43074  jm2.22  43836  clsk1indlem2  44882  nanorxor  45129  binomcxplemfrat  45175  binomcxplemradcnv  45176  pm10.251  45184  axc5c4c711toc7  45228  en3lpVD  45667  ax6e2ndeqVD  45731  2sb5ndVD  45732  ax6e2ndeqALT  45753  2sb5ndALT  45754  sineq0ALT  45759  axccdom  46052  fzdifsuc2  46143  liminf0  46621  cncfiooicc  46722  itgcoscmulx  46797  sge0sn  47207  isomenndlem  47358  hoidmvlelem2  47424  et-ltneverrefl  47699  quantgodelALT  47703  nabctnabc  47819  dfafv2  48020  afv2ndefb  48112  spr0el  48382  prmdvdsfmtnof1lem2  48488  fucofvalne  50251