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  2455  barocoALT  2702  necon3bi  2982  prcnel  3476  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  5270  snexALT  5345  csbopab  5530  nprrel12  5709  csbxp  5752  soirri  6120  predpoirr  6335  predfrirr  6336  nsuceq0  6447  csbiota  6530  eldifpw  7780  nlimsucg  7851  tfindsg  7870  findsg  7907  curry1val  8114  curry2val  8118  fsetdmprc0  8870  fiprc  9065  sdomirr  9126  domtriord  9135  2pwuninel  9144  mapdom1  9154  nfielex  9258  relprcnfsupp  9349  wemapso2  9540  card2inf  9542  en2lp  9600  wemapwe  9691  rankxplim3  9891  fidomtri2  10068  alephnbtwn  10143  kmlem2  10223  isfin7-2  10467  dominf  10516  ac6n  10556  alephval2  10650  dominfac  10651  gchdomtri  10707  nlt1pi  10984  indval0  12317  zeo  12778  bcpasc  14458  hashnemnf  14481  hasheq0  14500  hashunx  14523  hashbc  14591  pfxval0  14819  flodddiv4lt  16580  prmreclem4  17090  ressinbas  17416  natfval  18117  fucbas  18131  fuchom  18132  coafval  18232  efgval  19924  gsum2dlem1  20177  gsum2dlem2  20178  dprddomprc  20209  dprdval0prc  20211  isfieldidl  21533  psrvscafval  22249  mavmul0g  22861  mdetralt  22916  mdetunilem9  22928  matunitlindflem1  22987  cfinfil  24205  pcofval  25324  i1fima2  25993  i1fd  25995  itgeq2  26091  ibladdlem  26133  nbgrnself2  29934  clwwlknondisj  30695  nfrgr2v  30866  avril1  31057  nmobndseqi  31374  nonbooli  32246  chpssati  32958  nn0difffzod  33389  hashxpe  33392  gsumfs2d  33615  1arithufdlem4  34072  hasheuni  34710  ddemeas  34862  bnj1143  35413  fineqvnttrclse  35775  fineqvinfep  35776  kardval  35803  kard0b  35810  distel  36545  linedegen  36888  ordcmp  37215  bj-babygodel  37453  bj-nexrt  37574  bj-csbprc  37802  onsucuni3  38270  finxpnom  38304  wl-ifp-ncond1  38367  unccur  38506  poimirlem26  38544  poimirlem27  38545  poimirlem31  38549  cnambfre  38566  ibladdnclem  38574  frinfm  38649  tsbi3  39047  mopickr  39283  ax13fromc9  39943  axc711  39951  axc711toc7  39953  axc5c711toc7  39957  equidqe  39959  equidq  39961  ax12indalem  39982  hdmap1eulem  42859  hdmapevec  42872  intnanrt  43238  jm2.22  43981  clsk1indlem2  45027  nanorxor  45274  binomcxplemfrat  45320  binomcxplemradcnv  45321  pm10.251  45329  axc5c4c711toc7  45373  en3lpVD  45812  ax6e2ndeqVD  45876  2sb5ndVD  45877  ax6e2ndeqALT  45898  2sb5ndALT  45899  sineq0ALT  45904  axccdom  46204  fzdifsuc2  46295  liminf0  46772  cncfiooicc  46873  itgcoscmulx  46948  sge0sn  47358  isomenndlem  47509  hoidmvlelem2  47575  et-ltneverrefl  47850  quantgodelALT  47854  nabctnabc  47970  dfafv2  48171  afv2ndefb  48263  spr0el  48533  prmdvdsfmtnof1lem2  48639  fucofvalne  50402