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 ⊢ (¬ 𝜓 → ¬ 𝜑)

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  171  pm2.65iOLD  197  pm5.21ni  380  pm2.45  894  pm2.46  895  con3ALT  1099  rb-ax2  1780  rb-ax4  1782  emptyex  1934  excomimw  2071  naev  2089  ax13ALT  2463  barocoALT  2710  necon3bi  2990  prcnel  3488  sbc2or  3762  nel1nelin  4168  nel2nelin  4169  difrab  4279  sbcel12  4374  sbcne12  4378  sbcel2  4381  rexn0  4459  ifeqor  4541  ifan  4543  nelpri  4623  nelprd  4625  eqoreldif  4653  vneqv  5278  snexALT  5352  csbopab  5538  nprrel12  5717  csbxp  5760  soirri  6124  predpoirr  6332  predfrirr  6333  nsuceq0  6444  csbiota  6527  eldifpw  7763  nlimsucg  7834  tfindsg  7853  findsg  7890  curry1val  8096  curry2val  8100  fsetdmprc0  8848  fiprc  9037  sdomirr  9098  domtriord  9107  2pwuninel  9116  mapdom1  9126  nfielex  9230  relprcnfsupp  9320  wemapso2  9511  card2inf  9513  en2lp  9571  wemapwe  9662  rankxplim3  9849  fidomtri2  9976  alephnbtwn  10051  kmlem2  10131  isfin7-2  10376  dominf  10425  ac6n  10465  alephval2  10553  dominfac  10554  gchdomtri  10610  nlt1pi  10887  indval0  12218  zeo  12678  bcpasc  14353  hashnemnf  14376  hasheq0  14395  hashunx  14418  hashbc  14486  pfxval0  14710  flodddiv4lt  16471  prmreclem4  16975  ressinbas  17301  natfval  18002  fucbas  18016  fuchom  18017  coafval  18117  efgval  19783  gsum2dlem1  20036  gsum2dlem2  20037  dprddomprc  20068  dprdval0prc  20070  psrvscafval  22063  mavmul0g  22675  mdetralt  22730  mdetunilem9  22742  cfinfil  24015  pcofval  25134  i1fima2  25803  i1fd  25805  itgeq2  25902  ibladdlem  25944  nbgrnself2  29647  clwwlknondisj  30399  nfrgr2v  30560  avril1  30751  nmobndseqi  31068  nonbooli  31940  chpssati  32652  nn0difffzod  33086  hashxpe  33089  gsumfs2d  33318  1arithufdlem4  33778  hasheuni  34416  ddemeas  34567  bnj1143  35119  fineqvnttrclse  35456  fineqvinfep  35457  distel  36188  linedegen  36530  ordcmp  36843  bj-babygodel  37081  bj-nexrt  37202  bj-csbprc  37430  onsucuni3  37896  finxpnom  37930  wl-ifp-ncond1  37993  unccur  38137  matunitlindflem1  38150  poimirlem26  38180  poimirlem27  38181  poimirlem31  38185  cnambfre  38202  ibladdnclem  38210  frinfm  38269  tsbi3  38669  mopickr  38905  ax13fromc9  39565  axc711  39573  axc711toc7  39575  axc5c711toc7  39579  equidqe  39581  equidq  39583  ax12indalem  39604  hdmap1eulem  42481  hdmapevec  42494  intnanrt  42860  jm2.22  43609  clsk1indlem2  44655  nanorxor  44902  binomcxplemfrat  44948  binomcxplemradcnv  44949  pm10.251  44957  axc5c4c711toc7  45001  en3lpVD  45440  ax6e2ndeqVD  45504  2sb5ndVD  45505  ax6e2ndeqALT  45526  2sb5ndALT  45527  sineq0ALT  45532  axccdom  45825  fzdifsuc2  45916  liminf0  46394  cncfiooicc  46495  itgcoscmulx  46570  sge0sn  46980  isomenndlem  47131  hoidmvlelem2  47197  et-ltneverrefl  47472  quantgodelALT  47476  nabctnabc  47552  dfafv2  47753  afv2ndefb  47845  spr0el  48115  prmdvdsfmtnof1lem2  48221  fucofvalne  49983