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  3470  sbc2or  3759  nel1nelin  4166  nel2nelin  4167  difrab  4277  sbcel12  4370  sbcne12  4374  sbcel2  4377  rexn0  4470  ifeqor  4536  ifan  4538  nelpri  4615  nelprd  4617  eqoreldif  4645  snexALT  5333  csbopab  5510  nprrel12  5689  csbxp  5730  soirri  6087  predpoirr  6294  predfrirr  6295  nsuceq0  6405  csbiota  6492  eldifpw  7724  nlimsucg  7798  tfindsg  7817  findsg  7853  curry1val  8061  curry2val  8065  fsetdmprc0  8805  fiprc  8993  sdomirr  9055  domtriord  9064  2pwuninel  9073  mapdom1  9083  nfielex  9194  relprcnfsupp  9291  wemapso2  9482  card2inf  9484  en2lp  9535  wemapwe  9626  rankxplim3  9810  fidomtri2  9923  alephnbtwn  10000  kmlem2  10081  isfin7-2  10325  dominf  10374  ac6n  10414  alephval2  10501  dominfac  10502  gchdomtri  10558  nlt1pi  10835  zeo  12596  bcpasc  14262  hashnemnf  14285  hasheq0  14304  hashunx  14327  hashbc  14394  pfxval0  14617  flodddiv4lt  16363  prmreclem4  16866  ressinbas  17191  natfval  17887  fucbas  17901  fuchom  17902  coafval  18002  efgval  19623  gsum2dlem1  19876  gsum2dlem2  19877  dprddomprc  19908  dprdval0prc  19910  psrvscafval  21833  mavmul0g  22416  mdetralt  22471  mdetunilem9  22483  cfinfil  23756  pcofval  24886  i1fima2  25556  i1fd  25558  itgeq2  25655  ibladdlem  25697  nbgrnself2  29263  clwwlknondisj  30013  nfrgr2v  30174  avril1  30365  nmobndseqi  30681  nonbooli  31553  chpssati  32265  nn0difffzod  32702  hashxpe  32705  gsumfs2d  32968  1arithufdlem4  33491  hasheuni  34048  ddemeas  34199  bnj1143  34753  distel  35764  linedegen  36104  ordcmp  36408  bj-babygodel  36564  bj-nexrt  36653  bj-csbprc  36871  onsucuni3  37328  finxpnom  37362  wl-ifp-ncond1  37425  wl-ax11-lem8  37553  unccur  37570  matunitlindflem1  37583  poimirlem26  37613  poimirlem27  37614  poimirlem31  37618  cnambfre  37635  ibladdnclem  37643  frinfm  37702  tsbi3  38102  mopickr  38318  ax13fromc9  38872  axc711  38880  axc711toc7  38882  axc5c711toc7  38886  equidqe  38888  equidq  38890  ax12indalem  38911  hdmap1eulem  41789  hdmapevec  41802  intnanrt  42167  jm2.22  42957  clsk1indlem2  44004  nanorxor  44267  binomcxplemfrat  44313  binomcxplemradcnv  44314  pm10.251  44322  axc5c4c711toc7  44366  en3lpVD  44807  ax6e2ndeqVD  44871  2sb5ndVD  44872  ax6e2ndeqALT  44893  2sb5ndALT  44894  sineq0ALT  44899  axccdom  45189  fzdifsuc2  45281  liminf0  45764  cncfiooicc  45865  itgcoscmulx  45940  sge0sn  46350  isomenndlem  46501  hoidmvlelem2  46567  et-ltneverrefl  46842  singoutnword  46853  nabctnabc  46905  dfafv2  47106  afv2ndefb  47198  spr0el  47456  prmdvdsfmtnof1lem2  47559  fucofvalne  49287