Theorem con3i 154

Description: A contraposition inference. Inference associated with con3 153. Its associated inference is mto 197. (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 22	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con3i.a	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl 140	1 ⊢ (¬ 𝜓 → ¬ 𝜑)

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:  conax1  170  pm2.65i  194  pm5.21ni  377  pm2.45  881  pm2.46  882  con3ALT  1084  rb-ax2  1753  rb-ax4  1755  emptyex  1907  excomimw  2044  naev  2061  ax13ALT  2423  barocoALT  2670  necon3bi  2951  prcnel  3473  sbc2or  3762  nel1nelin  4170  nel2nelin  4171  difrab  4281  sbcel12  4374  sbcne12  4378  sbcel2  4381  rexn0  4474  ifeqor  4540  ifan  4542  nelpri  4619  nelprd  4621  eqoreldif  4649  snexALT  5338  csbopab  5515  nprrel12  5696  csbxp  5738  soirri  6099  predpoirr  6306  predfrirr  6307  nsuceq0  6417  csbiota  6504  eldifpw  7744  nlimsucg  7818  tfindsg  7837  findsg  7873  curry1val  8084  curry2val  8088  fsetdmprc0  8828  fiprc  9016  sdomirr  9078  domtriord  9087  2pwuninel  9096  mapdom1  9106  nfielex  9218  relprcnfsupp  9315  wemapso2  9506  card2inf  9508  en2lp  9559  wemapwe  9650  rankxplim3  9834  fidomtri2  9947  alephnbtwn  10024  kmlem2  10105  isfin7-2  10349  dominf  10398  ac6n  10438  alephval2  10525  dominfac  10526  gchdomtri  10582  nlt1pi  10859  zeo  12620  bcpasc  14286  hashnemnf  14309  hasheq0  14328  hashunx  14351  hashbc  14418  pfxval0  14641  flodddiv4lt  16387  prmreclem4  16890  ressinbas  17215  natfval  17911  fucbas  17925  fuchom  17926  coafval  18026  efgval  19647  gsum2dlem1  19900  gsum2dlem2  19901  dprddomprc  19932  dprdval0prc  19934  psrvscafval  21857  mavmul0g  22440  mdetralt  22495  mdetunilem9  22507  cfinfil  23780  pcofval  24910  i1fima2  25580  i1fd  25582  itgeq2  25679  ibladdlem  25721  nbgrnself2  29287  clwwlknondisj  30040  nfrgr2v  30201  avril1  30392  nmobndseqi  30708  nonbooli  31580  chpssati  32292  nn0difffzod  32729  hashxpe  32732  gsumfs2d  32995  1arithufdlem4  33518  hasheuni  34075  ddemeas  34226  bnj1143  34780  distel  35791  linedegen  36131  ordcmp  36435  bj-babygodel  36591  bj-nexrt  36680  bj-csbprc  36898  onsucuni3  37355  finxpnom  37389  wl-ifp-ncond1  37452  wl-ax11-lem8  37580  unccur  37597  matunitlindflem1  37610  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  cnambfre  37662  ibladdnclem  37670  frinfm  37729  tsbi3  38129  mopickr  38345  ax13fromc9  38899  axc711  38907  axc711toc7  38909  axc5c711toc7  38913  equidqe  38915  equidq  38917  ax12indalem  38938  hdmap1eulem  41816  hdmapevec  41829  intnanrt  42194  jm2.22  42984  clsk1indlem2  44031  nanorxor  44294  binomcxplemfrat  44340  binomcxplemradcnv  44341  pm10.251  44349  axc5c4c711toc7  44393  en3lpVD  44834  ax6e2ndeqVD  44898  2sb5ndVD  44899  ax6e2ndeqALT  44920  2sb5ndALT  44921  sineq0ALT  44926  axccdom  45216  fzdifsuc2  45308  liminf0  45791  cncfiooicc  45892  itgcoscmulx  45967  sge0sn  46377  isomenndlem  46528  hoidmvlelem2  46594  et-ltneverrefl  46869  singoutnword  46880  nabctnabc  46932  dfafv2  47133  afv2ndefb  47225  spr0el  47483  prmdvdsfmtnof1lem2  47586  fucofvalne  49314