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  2430  barocoALT  2678  necon3bi  2959  prcnel  3456  sbc2or  3738  nel1nelin  4148  nel2nelin  4149  difrab  4259  sbcel12  4352  sbcne12  4356  sbcel2  4359  rexn0  4437  ifeqor  4519  ifan  4521  nelpri  4600  nelprd  4602  eqoreldif  4630  snexALT  5318  csbopab  5501  nprrel12  5680  csbxp  5723  soirri  6081  predpoirr  6289  predfrirr  6290  nsuceq0  6400  csbiota  6483  eldifpw  7713  nlimsucg  7784  tfindsg  7803  findsg  7839  curry1val  8046  curry2val  8050  fsetdmprc0  8793  fiprc  8982  sdomirr  9043  domtriord  9052  2pwuninel  9061  mapdom1  9071  nfielex  9175  relprcnfsupp  9268  wemapso2  9459  card2inf  9461  en2lp  9516  wemapwe  9607  rankxplim3  9794  fidomtri2  9907  alephnbtwn  9982  kmlem2  10063  isfin7-2  10307  dominf  10356  ac6n  10396  alephval2  10484  dominfac  10485  gchdomtri  10541  nlt1pi  10818  zeo  12579  bcpasc  14245  hashnemnf  14268  hasheq0  14287  hashunx  14310  hashbc  14377  pfxval0  14601  flodddiv4lt  16345  prmreclem4  16848  ressinbas  17173  natfval  17874  fucbas  17888  fuchom  17889  coafval  17989  efgval  19650  gsum2dlem1  19903  gsum2dlem2  19904  dprddomprc  19935  dprdval0prc  19937  psrvscafval  21905  mavmul0g  22496  mdetralt  22551  mdetunilem9  22563  cfinfil  23836  pcofval  24955  i1fima2  25624  i1fd  25626  itgeq2  25723  ibladdlem  25765  nbgrnself2  29417  clwwlknondisj  30170  nfrgr2v  30331  avril1  30522  nmobndseqi  30839  nonbooli  31711  chpssati  32423  nn0difffzod  32867  hashxpe  32870  gsumfs2d  33127  1arithufdlem4  33612  hasheuni  34235  ddemeas  34386  bnj1143  34938  fineqvnttrclse  35274  fineqvinfep  35275  distel  35989  linedegen  36331  ordcmp  36635  bj-babygodel  36866  bj-nexrt  36987  bj-csbprc  37215  onsucuni3  37679  finxpnom  37713  wl-ifp-ncond1  37776  unccur  37915  matunitlindflem1  37928  poimirlem26  37958  poimirlem27  37959  poimirlem31  37963  cnambfre  37980  ibladdnclem  37988  frinfm  38047  tsbi3  38447  mopickr  38683  ax13fromc9  39343  axc711  39351  axc711toc7  39353  axc5c711toc7  39357  equidqe  39359  equidq  39361  ax12indalem  39382  hdmap1eulem  42259  hdmapevec  42272  intnanrt  42637  jm2.22  43426  clsk1indlem2  44472  nanorxor  44735  binomcxplemfrat  44781  binomcxplemradcnv  44782  pm10.251  44790  axc5c4c711toc7  44834  en3lpVD  45274  ax6e2ndeqVD  45338  2sb5ndVD  45339  ax6e2ndeqALT  45360  2sb5ndALT  45361  sineq0ALT  45366  axccdom  45654  fzdifsuc2  45746  liminf0  46225  cncfiooicc  46326  itgcoscmulx  46401  sge0sn  46811  isomenndlem  46962  hoidmvlelem2  47028  et-ltneverrefl  47303  nabctnabc  47365  dfafv2  47566  afv2ndefb  47658  spr0el  47916  prmdvdsfmtnof1lem2  48019  fucofvalne  49758