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  5320  csbopab  5503  nprrel12  5682  csbxp  5725  soirri  6083  predpoirr  6291  predfrirr  6292  nsuceq0  6402  csbiota  6485  eldifpw  7715  nlimsucg  7786  tfindsg  7805  findsg  7841  curry1val  8048  curry2val  8052  fsetdmprc0  8795  fiprc  8984  sdomirr  9045  domtriord  9054  2pwuninel  9063  mapdom1  9073  nfielex  9177  relprcnfsupp  9270  wemapso2  9461  card2inf  9463  en2lp  9518  wemapwe  9609  rankxplim3  9796  fidomtri2  9909  alephnbtwn  9984  kmlem2  10065  isfin7-2  10309  dominf  10358  ac6n  10398  alephval2  10486  dominfac  10487  gchdomtri  10543  nlt1pi  10820  indval0  12154  zeo  12606  bcpasc  14274  hashnemnf  14297  hasheq0  14316  hashunx  14339  hashbc  14406  pfxval0  14630  flodddiv4lt  16377  prmreclem4  16881  ressinbas  17206  natfval  17907  fucbas  17921  fuchom  17922  coafval  18022  efgval  19683  gsum2dlem1  19936  gsum2dlem2  19937  dprddomprc  19968  dprdval0prc  19970  psrvscafval  21937  mavmul0g  22528  mdetralt  22583  mdetunilem9  22595  cfinfil  23868  pcofval  24987  i1fima2  25656  i1fd  25658  itgeq2  25755  ibladdlem  25797  nbgrnself2  29443  clwwlknondisj  30196  nfrgr2v  30357  avril1  30548  nmobndseqi  30865  nonbooli  31737  chpssati  32449  nn0difffzod  32892  hashxpe  32895  gsumfs2d  33137  1arithufdlem4  33622  hasheuni  34245  ddemeas  34396  bnj1143  34948  fineqvnttrclse  35284  fineqvinfep  35285  distel  35999  linedegen  36341  ordcmp  36645  bj-babygodel  36884  bj-nexrt  37005  bj-csbprc  37233  onsucuni3  37697  finxpnom  37731  wl-ifp-ncond1  37794  unccur  37938  matunitlindflem1  37951  poimirlem26  37981  poimirlem27  37982  poimirlem31  37986  cnambfre  38003  ibladdnclem  38011  frinfm  38070  tsbi3  38470  mopickr  38706  ax13fromc9  39366  axc711  39374  axc711toc7  39376  axc5c711toc7  39380  equidqe  39382  equidq  39384  ax12indalem  39405  hdmap1eulem  42282  hdmapevec  42295  intnanrt  42659  jm2.22  43441  clsk1indlem2  44487  nanorxor  44750  binomcxplemfrat  44796  binomcxplemradcnv  44797  pm10.251  44805  axc5c4c711toc7  44849  en3lpVD  45289  ax6e2ndeqVD  45353  2sb5ndVD  45354  ax6e2ndeqALT  45375  2sb5ndALT  45376  sineq0ALT  45381  axccdom  45669  fzdifsuc2  45761  liminf0  46239  cncfiooicc  46340  itgcoscmulx  46415  sge0sn  46825  isomenndlem  46976  hoidmvlelem2  47042  et-ltneverrefl  47317  nabctnabc  47391  dfafv2  47592  afv2ndefb  47684  spr0el  47954  prmdvdsfmtnof1lem2  48060  fucofvalne  49812