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  882  pm2.46  883  con3ALT  1085  rb-ax2  1755  rb-ax4  1757  emptyex  1909  excomimw  2046  naev  2064  ax13ALT  2429  barocoALT  2677  necon3bi  2958  prcnel  3455  sbc2or  3737  nel1nelin  4147  nel2nelin  4148  difrab  4258  sbcel12  4351  sbcne12  4355  sbcel2  4358  rexn0  4436  ifeqor  4518  ifan  4520  nelpri  4599  nelprd  4601  eqoreldif  4629  vneqv  5251  snexALT  5325  csbopab  5510  nprrel12  5689  csbxp  5732  soirri  6089  predpoirr  6297  predfrirr  6298  nsuceq0  6408  csbiota  6491  eldifpw  7722  nlimsucg  7793  tfindsg  7812  findsg  7848  curry1val  8055  curry2val  8059  fsetdmprc0  8802  fiprc  8991  sdomirr  9052  domtriord  9061  2pwuninel  9070  mapdom1  9080  nfielex  9184  relprcnfsupp  9277  wemapso2  9468  card2inf  9470  en2lp  9527  wemapwe  9618  rankxplim3  9805  fidomtri2  9918  alephnbtwn  9993  kmlem2  10074  isfin7-2  10318  dominf  10367  ac6n  10407  alephval2  10495  dominfac  10496  gchdomtri  10552  nlt1pi  10829  indval0  12163  zeo  12615  bcpasc  14283  hashnemnf  14306  hasheq0  14325  hashunx  14348  hashbc  14415  pfxval0  14639  flodddiv4lt  16386  prmreclem4  16890  ressinbas  17215  natfval  17916  fucbas  17930  fuchom  17931  coafval  18031  efgval  19692  gsum2dlem1  19945  gsum2dlem2  19946  dprddomprc  19977  dprdval0prc  19979  psrvscafval  21927  mavmul0g  22518  mdetralt  22573  mdetunilem9  22585  cfinfil  23858  pcofval  24977  i1fima2  25646  i1fd  25648  itgeq2  25745  ibladdlem  25787  nbgrnself2  29429  clwwlknondisj  30181  nfrgr2v  30342  avril1  30533  nmobndseqi  30850  nonbooli  31722  chpssati  32434  nn0difffzod  32877  hashxpe  32880  gsumfs2d  33122  1arithufdlem4  33607  hasheuni  34229  ddemeas  34380  bnj1143  34932  fineqvnttrclse  35268  fineqvinfep  35269  distel  35983  linedegen  36325  ordcmp  36629  bj-babygodel  36868  bj-nexrt  36989  bj-csbprc  37217  onsucuni3  37683  finxpnom  37717  wl-ifp-ncond1  37780  unccur  37924  matunitlindflem1  37937  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  cnambfre  37989  ibladdnclem  37997  frinfm  38056  tsbi3  38456  mopickr  38692  ax13fromc9  39352  axc711  39360  axc711toc7  39362  axc5c711toc7  39366  equidqe  39368  equidq  39370  ax12indalem  39391  hdmap1eulem  42268  hdmapevec  42281  intnanrt  42645  jm2.22  43423  clsk1indlem2  44469  nanorxor  44732  binomcxplemfrat  44778  binomcxplemradcnv  44779  pm10.251  44787  axc5c4c711toc7  44831  en3lpVD  45271  ax6e2ndeqVD  45335  2sb5ndVD  45336  ax6e2ndeqALT  45357  2sb5ndALT  45358  sineq0ALT  45363  axccdom  45651  fzdifsuc2  45743  liminf0  46221  cncfiooicc  46322  itgcoscmulx  46397  sge0sn  46807  isomenndlem  46958  hoidmvlelem2  47024  et-ltneverrefl  47299  quantgodelALT  47303  nabctnabc  47379  dfafv2  47580  afv2ndefb  47672  spr0el  47942  prmdvdsfmtnof1lem2  48048  fucofvalne  49800