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  1753  rb-ax4  1755  emptyex  1907  excomimw  2044  naev  2061  ax13ALT  2423  barocoALT  2670  necon3bi  2951  prcnel  3464  sbc2or  3753  nel1nelin  4160  nel2nelin  4161  difrab  4271  sbcel12  4364  sbcne12  4368  sbcel2  4371  rexn0  4464  ifeqor  4530  ifan  4532  nelpri  4609  nelprd  4611  eqoreldif  4639  snexALT  5325  csbopab  5502  nprrel12  5681  csbxp  5723  soirri  6079  predpoirr  6285  predfrirr  6286  nsuceq0  6396  csbiota  6479  eldifpw  7708  nlimsucg  7782  tfindsg  7801  findsg  7837  curry1val  8045  curry2val  8049  fsetdmprc0  8789  fiprc  8977  sdomirr  9038  domtriord  9047  2pwuninel  9056  mapdom1  9066  nfielex  9176  relprcnfsupp  9273  wemapso2  9464  card2inf  9466  en2lp  9521  wemapwe  9612  rankxplim3  9796  fidomtri2  9909  alephnbtwn  9984  kmlem2  10065  isfin7-2  10309  dominf  10358  ac6n  10398  alephval2  10485  dominfac  10486  gchdomtri  10542  nlt1pi  10819  zeo  12581  bcpasc  14247  hashnemnf  14270  hasheq0  14289  hashunx  14312  hashbc  14379  pfxval0  14602  flodddiv4lt  16347  prmreclem4  16850  ressinbas  17175  natfval  17875  fucbas  17889  fuchom  17890  coafval  17990  efgval  19615  gsum2dlem1  19868  gsum2dlem2  19869  dprddomprc  19900  dprdval0prc  19902  psrvscafval  21874  mavmul0g  22457  mdetralt  22512  mdetunilem9  22524  cfinfil  23797  pcofval  24927  i1fima2  25597  i1fd  25599  itgeq2  25696  ibladdlem  25738  nbgrnself2  29324  clwwlknondisj  30074  nfrgr2v  30235  avril1  30426  nmobndseqi  30742  nonbooli  31614  chpssati  32326  nn0difffzod  32768  hashxpe  32771  gsumfs2d  33027  1arithufdlem4  33503  hasheuni  34071  ddemeas  34222  bnj1143  34776  distel  35796  linedegen  36136  ordcmp  36440  bj-babygodel  36596  bj-nexrt  36685  bj-csbprc  36903  onsucuni3  37360  finxpnom  37394  wl-ifp-ncond1  37457  wl-ax11-lem8  37585  unccur  37602  matunitlindflem1  37615  poimirlem26  37645  poimirlem27  37646  poimirlem31  37650  cnambfre  37667  ibladdnclem  37675  frinfm  37734  tsbi3  38134  mopickr  38350  ax13fromc9  38904  axc711  38912  axc711toc7  38914  axc5c711toc7  38918  equidqe  38920  equidq  38922  ax12indalem  38943  hdmap1eulem  41821  hdmapevec  41834  intnanrt  42199  jm2.22  42988  clsk1indlem2  44035  nanorxor  44298  binomcxplemfrat  44344  binomcxplemradcnv  44345  pm10.251  44353  axc5c4c711toc7  44397  en3lpVD  44838  ax6e2ndeqVD  44902  2sb5ndVD  44903  ax6e2ndeqALT  44924  2sb5ndALT  44925  sineq0ALT  44930  axccdom  45220  fzdifsuc2  45312  liminf0  45794  cncfiooicc  45895  itgcoscmulx  45970  sge0sn  46380  isomenndlem  46531  hoidmvlelem2  46597  et-ltneverrefl  46872  singoutnword  46883  nabctnabc  46935  dfafv2  47136  afv2ndefb  47228  spr0el  47486  prmdvdsfmtnof1lem2  47589  fucofvalne  49330