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  6336  predfrirr  6337  nsuceq0  6448  csbiota  6531  eldifpw  7782  nlimsucg  7853  tfindsg  7872  findsg  7909  curry1val  8116  curry2val  8120  fsetdmprc0  8877  fiprc  9072  sdomirr  9133  domtriord  9142  2pwuninel  9151  mapdom1  9161  nfielex  9265  relprcnfsupp  9356  wemapso2  9547  card2inf  9549  en2lp  9607  wemapwe  9698  rankxplim3  9898  fidomtri2  10075  alephnbtwn  10150  kmlem2  10230  isfin7-2  10474  dominf  10523  ac6n  10563  alephval2  10657  dominfac  10658  gchdomtri  10714  nlt1pi  10991  indval0  12324  zeo  12785  bcpasc  14465  hashnemnf  14488  hasheq0  14507  hashunx  14530  hashbc  14598  pfxval0  14826  flodddiv4lt  16587  prmreclem4  17097  ressinbas  17423  natfval  18124  fucbas  18138  fuchom  18139  coafval  18239  efgval  19931  gsum2dlem1  20184  gsum2dlem2  20185  dprddomprc  20216  dprdval0prc  20218  isfieldidl  21540  psrvscafval  22256  mavmul0g  22868  mdetralt  22923  mdetunilem9  22935  matunitlindflem1  22994  cfinfil  24212  pcofval  25331  i1fima2  26000  i1fd  26002  itgeq2  26098  ibladdlem  26140  nbgrnself2  29941  clwwlknondisj  30702  nfrgr2v  30873  avril1  31064  nmobndseqi  31381  nonbooli  32253  chpssati  32965  nn0difffzod  33396  hashxpe  33399  gsumfs2d  33622  1arithufdlem4  34079  hasheuni  34717  ddemeas  34869  bnj1143  35420  fineqvnttrclse  35792  fineqvinfep  35793  kardval  35820  kard0b  35827  distel  36565  linedegen  36908  ordcmp  37235  bj-babygodel  37473  bj-nexrt  37594  bj-csbprc  37822  onsucuni3  38291  finxpnom  38325  wl-ifp-ncond1  38388  unccur  38527  poimirlem26  38565  poimirlem27  38566  poimirlem31  38570  cnambfre  38587  ibladdnclem  38595  frinfm  38670  tsbi3  39068  mopickr  39304  ax13fromc9  39964  axc711  39972  axc711toc7  39974  axc5c711toc7  39978  equidqe  39980  equidq  39982  ax12indalem  40003  hdmap1eulem  42880  hdmapevec  42893  intnanrt  43259  jm2.22  44002  clsk1indlem2  45042  nanorxor  45289  binomcxplemfrat  45335  binomcxplemradcnv  45336  pm10.251  45344  axc5c4c711toc7  45388  en3lpVD  45827  ax6e2ndeqVD  45891  2sb5ndVD  45892  ax6e2ndeqALT  45913  2sb5ndALT  45914  sineq0ALT  45919  axccdom  46235  fzdifsuc2  46326  liminf0  46803  cncfiooicc  46904  itgcoscmulx  46979  sge0sn  47389  isomenndlem  47540  hoidmvlelem2  47606  et-ltneverrefl  47881  quantgodelALT  47885  nabctnabc  48001  dfafv2  48202  afv2ndefb  48294  spr0el  48564  prmdvdsfmtnof1lem2  48670  fucofvalne  50433