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  1754  rb-ax4  1756  emptyex  1908  excomimw  2045  naev  2063  ax13ALT  2429  barocoALT  2677  necon3bi  2958  prcnel  3466  sbc2or  3749  nel1nelin  4159  nel2nelin  4160  difrab  4270  sbcel12  4363  sbcne12  4367  sbcel2  4370  rexn0  4449  ifeqor  4531  ifan  4533  nelpri  4612  nelprd  4614  eqoreldif  4642  snexALT  5328  csbopab  5503  nprrel12  5682  csbxp  5725  soirri  6083  predpoirr  6291  predfrirr  6292  nsuceq0  6402  csbiota  6485  eldifpw  7713  nlimsucg  7784  tfindsg  7803  findsg  7839  curry1val  8047  curry2val  8051  fsetdmprc0  8792  fiprc  8981  sdomirr  9042  domtriord  9051  2pwuninel  9060  mapdom1  9070  nfielex  9174  relprcnfsupp  9267  wemapso2  9458  card2inf  9460  en2lp  9515  wemapwe  9606  rankxplim3  9793  fidomtri2  9906  alephnbtwn  9981  kmlem2  10062  isfin7-2  10306  dominf  10355  ac6n  10395  alephval2  10483  dominfac  10484  gchdomtri  10540  nlt1pi  10817  zeo  12578  bcpasc  14244  hashnemnf  14267  hasheq0  14286  hashunx  14309  hashbc  14376  pfxval0  14600  flodddiv4lt  16344  prmreclem4  16847  ressinbas  17172  natfval  17873  fucbas  17887  fuchom  17888  coafval  17988  efgval  19646  gsum2dlem1  19899  gsum2dlem2  19900  dprddomprc  19931  dprdval0prc  19933  psrvscafval  21904  mavmul0g  22497  mdetralt  22552  mdetunilem9  22564  cfinfil  23837  pcofval  24966  i1fima2  25636  i1fd  25638  itgeq2  25735  ibladdlem  25777  nbgrnself2  29433  clwwlknondisj  30186  nfrgr2v  30347  avril1  30538  nmobndseqi  30854  nonbooli  31726  chpssati  32438  nn0difffzod  32884  hashxpe  32887  gsumfs2d  33144  1arithufdlem4  33628  hasheuni  34242  ddemeas  34393  bnj1143  34946  fineqvnttrclse  35280  fineqvinfep  35281  distel  35995  linedegen  36337  ordcmp  36641  bj-babygodel  36803  bj-nexrt  36893  bj-csbprc  37111  onsucuni3  37572  finxpnom  37606  wl-ifp-ncond1  37669  unccur  37804  matunitlindflem1  37817  poimirlem26  37847  poimirlem27  37848  poimirlem31  37852  cnambfre  37869  ibladdnclem  37877  frinfm  37936  tsbi3  38336  mopickr  38556  ax13fromc9  39166  axc711  39174  axc711toc7  39176  axc5c711toc7  39180  equidqe  39182  equidq  39184  ax12indalem  39205  hdmap1eulem  42082  hdmapevec  42095  intnanrt  42460  jm2.22  43237  clsk1indlem2  44283  nanorxor  44546  binomcxplemfrat  44592  binomcxplemradcnv  44593  pm10.251  44601  axc5c4c711toc7  44645  en3lpVD  45085  ax6e2ndeqVD  45149  2sb5ndVD  45150  ax6e2ndeqALT  45171  2sb5ndALT  45172  sineq0ALT  45177  axccdom  45466  fzdifsuc2  45558  liminf0  46037  cncfiooicc  46138  itgcoscmulx  46213  sge0sn  46623  isomenndlem  46774  hoidmvlelem2  46840  et-ltneverrefl  47115  nabctnabc  47177  dfafv2  47378  afv2ndefb  47470  spr0el  47728  prmdvdsfmtnof1lem2  47831  fucofvalne  49570