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  1753  rb-ax4  1755  emptyex  1907  excomimw  2043  naev  2060  ax13ALT  2430  barocoALT  2677  necon3bi  2967  prcnel  3507  sbc2or  3797  nel1nelin  4207  nel2nelin  4208  difrab  4318  sbcel12  4411  sbcne12  4415  sbcel2  4418  rexn0  4511  ifeqor  4577  ifan  4579  nelpri  4655  nelprd  4657  eqoreldif  4685  snexALT  5383  csbopab  5560  nprrel12  5743  csbxp  5785  soirri  6146  predpoirr  6354  predfrirr  6355  nsuceq0  6467  csbiota  6554  eldifpw  7788  nlimsucg  7863  tfindsg  7882  findsg  7919  curry1val  8130  curry2val  8134  fsetdmprc0  8895  fiprc  9085  sdomirr  9154  domtriord  9163  2pwuninel  9172  mapdom1  9182  nfielex  9307  relprcnfsupp  9404  wemapso2  9593  card2inf  9595  en2lp  9646  wemapwe  9737  rankxplim3  9921  fidomtri2  10034  alephnbtwn  10111  kmlem2  10192  isfin7-2  10436  dominf  10485  ac6n  10525  alephval2  10612  dominfac  10613  gchdomtri  10669  nlt1pi  10946  zeo  12704  bcpasc  14360  hashnemnf  14383  hasheq0  14402  hashunx  14425  hashbc  14492  pfxval0  14714  flodddiv4lt  16454  prmreclem4  16957  ressinbas  17291  natfval  17994  fucbas  18008  fuchom  18009  coafval  18109  efgval  19735  gsum2dlem1  19988  gsum2dlem2  19989  dprddomprc  20020  dprdval0prc  20022  psrvscafval  21968  mavmul0g  22559  mdetralt  22614  mdetunilem9  22626  cfinfil  23901  pcofval  25043  i1fima2  25714  i1fd  25716  itgeq2  25813  ibladdlem  25855  nbgrnself2  29377  clwwlknondisj  30130  nfrgr2v  30291  avril1  30482  nmobndseqi  30798  nonbooli  31670  chpssati  32382  nn0difffzod  32808  hashxpe  32811  gsumfs2d  33058  1arithufdlem4  33575  hasheuni  34086  ddemeas  34237  bnj1143  34804  distel  35804  linedegen  36144  ordcmp  36448  bj-babygodel  36604  bj-nexrt  36693  bj-csbprc  36911  onsucuni3  37368  finxpnom  37402  wl-ifp-ncond1  37465  wl-ax11-lem8  37593  unccur  37610  matunitlindflem1  37623  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  cnambfre  37675  ibladdnclem  37683  frinfm  37742  tsbi3  38142  mopickr  38364  ax13fromc9  38907  axc711  38915  axc711toc7  38917  axc5c711toc7  38921  equidqe  38923  equidq  38925  ax12indalem  38946  hdmap1eulem  41824  hdmapevec  41837  intnanrt  42245  jm2.22  43007  clsk1indlem2  44055  nanorxor  44324  binomcxplemfrat  44370  binomcxplemradcnv  44371  pm10.251  44379  axc5c4c711toc7  44423  en3lpVD  44865  ax6e2ndeqVD  44929  2sb5ndVD  44930  ax6e2ndeqALT  44951  2sb5ndALT  44952  sineq0ALT  44957  axccdom  45227  fzdifsuc2  45322  liminf0  45808  cncfiooicc  45909  itgcoscmulx  45984  sge0sn  46394  isomenndlem  46545  hoidmvlelem2  46611  et-ltneverrefl  46886  singoutnword  46897  nabctnabc  46943  dfafv2  47144  afv2ndefb  47236  spr0el  47469  prmdvdsfmtnof1lem2  47572  fucofvalne  49020