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  2430  barocoALT  2677  necon3bi  2959  prcnel  3491  sbc2or  3779  nel1nelin  4187  nel2nelin  4188  difrab  4298  sbcel12  4391  sbcne12  4395  sbcel2  4398  rexn0  4491  ifeqor  4557  ifan  4559  nelpri  4636  nelprd  4638  eqoreldif  4666  snexALT  5358  csbopab  5535  nprrel12  5717  csbxp  5759  soirri  6120  predpoirr  6327  predfrirr  6328  nsuceq0  6442  csbiota  6529  eldifpw  7767  nlimsucg  7842  tfindsg  7861  findsg  7898  curry1val  8109  curry2val  8113  fsetdmprc0  8874  fiprc  9064  sdomirr  9133  domtriord  9142  2pwuninel  9151  mapdom1  9161  nfielex  9284  relprcnfsupp  9381  wemapso2  9572  card2inf  9574  en2lp  9625  wemapwe  9716  rankxplim3  9900  fidomtri2  10013  alephnbtwn  10090  kmlem2  10171  isfin7-2  10415  dominf  10464  ac6n  10504  alephval2  10591  dominfac  10592  gchdomtri  10648  nlt1pi  10925  zeo  12684  bcpasc  14344  hashnemnf  14367  hasheq0  14386  hashunx  14409  hashbc  14476  pfxval0  14699  flodddiv4lt  16441  prmreclem4  16944  ressinbas  17271  natfval  17967  fucbas  17981  fuchom  17982  coafval  18082  efgval  19703  gsum2dlem1  19956  gsum2dlem2  19957  dprddomprc  19988  dprdval0prc  19990  psrvscafval  21913  mavmul0g  22496  mdetralt  22551  mdetunilem9  22563  cfinfil  23836  pcofval  24966  i1fima2  25637  i1fd  25639  itgeq2  25736  ibladdlem  25778  nbgrnself2  29344  clwwlknondisj  30097  nfrgr2v  30258  avril1  30449  nmobndseqi  30765  nonbooli  31637  chpssati  32349  nn0difffzod  32788  hashxpe  32791  gsumfs2d  33054  1arithufdlem4  33567  hasheuni  34121  ddemeas  34272  bnj1143  34826  distel  35826  linedegen  36166  ordcmp  36470  bj-babygodel  36626  bj-nexrt  36715  bj-csbprc  36933  onsucuni3  37390  finxpnom  37424  wl-ifp-ncond1  37487  wl-ax11-lem8  37615  unccur  37632  matunitlindflem1  37645  poimirlem26  37675  poimirlem27  37676  poimirlem31  37680  cnambfre  37697  ibladdnclem  37705  frinfm  37764  tsbi3  38164  mopickr  38386  ax13fromc9  38929  axc711  38937  axc711toc7  38939  axc5c711toc7  38943  equidqe  38945  equidq  38947  ax12indalem  38968  hdmap1eulem  41846  hdmapevec  41859  intnanrt  42224  jm2.22  42986  clsk1indlem2  44033  nanorxor  44296  binomcxplemfrat  44342  binomcxplemradcnv  44343  pm10.251  44351  axc5c4c711toc7  44395  en3lpVD  44836  ax6e2ndeqVD  44900  2sb5ndVD  44901  ax6e2ndeqALT  44922  2sb5ndALT  44923  sineq0ALT  44928  axccdom  45213  fzdifsuc2  45306  liminf0  45789  cncfiooicc  45890  itgcoscmulx  45965  sge0sn  46375  isomenndlem  46526  hoidmvlelem2  46592  et-ltneverrefl  46867  singoutnword  46878  nabctnabc  46927  dfafv2  47128  afv2ndefb  47220  spr0el  47463  prmdvdsfmtnof1lem2  47566  fucofvalne  49203