Theorem con3i 154

Description: A contraposition inference. Inference associated with con3 153. Its associated inference is mto 198. (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  195  pm5.21ni  378  pm2.45  887  pm2.46  888  con3ALT  1090  rb-ax2  1760  rb-ax4  1762  emptyex  1914  excomimw  2051  naev  2069  ax13ALT  2433  barocoALT  2680  necon3bi  2960  prcnel  3456  sbc2or  3732  nel1nelin  4136  nel2nelin  4137  difrab  4246  sbcel12  4339  sbcne12  4343  sbcel2  4346  rexn0  4424  ifeqor  4506  ifan  4508  nelpri  4587  nelprd  4589  eqoreldif  4617  vneqv  5238  snexALT  5312  csbopab  5497  nprrel12  5676  csbxp  5719  soirri  6076  predpoirr  6284  predfrirr  6285  nsuceq0  6395  csbiota  6478  eldifpw  7711  nlimsucg  7782  tfindsg  7801  findsg  7837  curry1val  8044  curry2val  8048  fsetdmprc0  8792  fiprc  8981  sdomirr  9042  domtriord  9051  2pwuninel  9060  mapdom1  9070  nfielex  9174  relprcnfsupp  9267  wemapso2  9458  card2inf  9460  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  21923  mavmul0g  22536  mdetralt  22591  mdetunilem9  22603  cfinfil  23876  pcofval  24995  i1fima2  25664  i1fd  25666  itgeq2  25763  ibladdlem  25805  nbgrnself2  29447  clwwlknondisj  30199  nfrgr2v  30360  avril1  30551  nmobndseqi  30868  nonbooli  31740  chpssati  32452  nn0difffzod  32896  hashxpe  32899  gsumfs2d  33142  1arithufdlem4  33630  hasheuni  34269  ddemeas  34420  bnj1143  34972  fineqvnttrclse  35305  fineqvinfep  35306  distel  36029  linedegen  36371  ordcmp  36675  bj-babygodel  36914  bj-nexrt  37035  bj-csbprc  37263  onsucuni3  37729  finxpnom  37763  wl-ifp-ncond1  37826  unccur  37970  matunitlindflem1  37983  poimirlem26  38013  poimirlem27  38014  poimirlem31  38018  cnambfre  38035  ibladdnclem  38043  frinfm  38102  tsbi3  38502  mopickr  38738  ax13fromc9  39398  axc711  39406  axc711toc7  39408  axc5c711toc7  39412  equidqe  39414  equidq  39416  ax12indalem  39437  hdmap1eulem  42314  hdmapevec  42327  intnanrt  42691  jm2.22  43440  clsk1indlem2  44486  nanorxor  44749  binomcxplemfrat  44795  binomcxplemradcnv  44796  pm10.251  44804  axc5c4c711toc7  44848  en3lpVD  45288  ax6e2ndeqVD  45352  2sb5ndVD  45353  ax6e2ndeqALT  45374  2sb5ndALT  45375  sineq0ALT  45380  axccdom  45667  fzdifsuc2  45758  liminf0  46236  cncfiooicc  46337  itgcoscmulx  46412  sge0sn  46822  isomenndlem  46973  hoidmvlelem2  47039  et-ltneverrefl  47314  quantgodelALT  47318  nabctnabc  47394  dfafv2  47595  afv2ndefb  47687  spr0el  47957  prmdvdsfmtnof1lem2  48063  fucofvalne  49815