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  3468  sbc2or  3751  nel1nelin  4161  nel2nelin  4162  difrab  4272  sbcel12  4365  sbcne12  4369  sbcel2  4372  rexn0  4451  ifeqor  4533  ifan  4535  nelpri  4614  nelprd  4616  eqoreldif  4644  snexALT  5330  csbopab  5511  nprrel12  5690  csbxp  5733  soirri  6091  predpoirr  6299  predfrirr  6300  nsuceq0  6410  csbiota  6493  eldifpw  7723  nlimsucg  7794  tfindsg  7813  findsg  7849  curry1val  8057  curry2val  8061  fsetdmprc0  8804  fiprc  8993  sdomirr  9054  domtriord  9063  2pwuninel  9072  mapdom1  9082  nfielex  9186  relprcnfsupp  9279  wemapso2  9470  card2inf  9472  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  zeo  12590  bcpasc  14256  hashnemnf  14279  hasheq0  14298  hashunx  14321  hashbc  14388  pfxval0  14612  flodddiv4lt  16356  prmreclem4  16859  ressinbas  17184  natfval  17885  fucbas  17899  fuchom  17900  coafval  18000  efgval  19658  gsum2dlem1  19911  gsum2dlem2  19912  dprddomprc  19943  dprdval0prc  19945  psrvscafval  21916  mavmul0g  22509  mdetralt  22564  mdetunilem9  22576  cfinfil  23849  pcofval  24978  i1fima2  25648  i1fd  25650  itgeq2  25747  ibladdlem  25789  nbgrnself2  29445  clwwlknondisj  30198  nfrgr2v  30359  avril1  30550  nmobndseqi  30867  nonbooli  31739  chpssati  32451  nn0difffzod  32895  hashxpe  32898  gsumfs2d  33155  1arithufdlem4  33640  hasheuni  34263  ddemeas  34414  bnj1143  34966  fineqvnttrclse  35302  fineqvinfep  35303  distel  36017  linedegen  36359  ordcmp  36663  bj-babygodel  36828  bj-nexrt  36937  bj-csbprc  37158  onsucuni3  37622  finxpnom  37656  wl-ifp-ncond1  37719  unccur  37854  matunitlindflem1  37867  poimirlem26  37897  poimirlem27  37898  poimirlem31  37902  cnambfre  37919  ibladdnclem  37927  frinfm  37986  tsbi3  38386  mopickr  38622  ax13fromc9  39282  axc711  39290  axc711toc7  39292  axc5c711toc7  39296  equidqe  39298  equidq  39300  ax12indalem  39321  hdmap1eulem  42198  hdmapevec  42211  intnanrt  42576  jm2.22  43352  clsk1indlem2  44398  nanorxor  44661  binomcxplemfrat  44707  binomcxplemradcnv  44708  pm10.251  44716  axc5c4c711toc7  44760  en3lpVD  45200  ax6e2ndeqVD  45264  2sb5ndVD  45265  ax6e2ndeqALT  45286  2sb5ndALT  45287  sineq0ALT  45292  axccdom  45580  fzdifsuc2  45672  liminf0  46151  cncfiooicc  46252  itgcoscmulx  46327  sge0sn  46737  isomenndlem  46888  hoidmvlelem2  46954  et-ltneverrefl  47229  nabctnabc  47291  dfafv2  47492  afv2ndefb  47584  spr0el  47842  prmdvdsfmtnof1lem2  47945  fucofvalne  49684