Theorem con3i 154

Description: A contraposition inference. Inference associated with con3 153. Its associated inference is mto 196. (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  193  pm5.21ni  376  pm2.45  879  pm2.46  880  con3ALT  1082  rb-ax2  1747  rb-ax4  1749  emptyex  1902  naev  2055  ax13ALT  2418  barocoALT  2665  necon3bi  2956  prcnel  3486  sbc2or  3782  difrab  4307  sbcel12  4410  sbcne12  4414  sbcel2  4417  rexn0  4512  ifeqor  4581  ifan  4583  nelpri  4659  nelprd  4661  eqoreldif  4690  snexALT  5383  csbopab  5557  nprrel12  5736  csbxp  5777  soirri  6133  predpoirr  6341  predfrirr  6342  nsuceq0  6454  csbiota  6542  eldifpw  7771  nlimsucg  7847  tfindsg  7866  findsg  7905  curry1val  8110  curry2val  8114  fsetdmprc0  8874  fiprc  9073  sdomirr  9142  domtriord  9151  2pwuninel  9160  mapdom1  9170  nfielex  9301  relprcnfsupp  9395  wemapso2  9583  card2inf  9585  en2lp  9636  wemapwe  9727  rankxplim3  9911  fidomtri2  10024  alephnbtwn  10101  kmlem2  10181  isfin7-2  10426  dominf  10475  ac6n  10515  alephval2  10602  dominfac  10603  gchdomtri  10659  nlt1pi  10936  zeo  12686  bcpasc  14321  hashnemnf  14344  hasheq0  14363  hashunx  14386  hashbc  14453  pfxval0  14667  flodddiv4lt  16400  prmreclem4  16896  ressinbas  17234  natfval  17944  fucbas  17959  fuchom  17960  fuchomOLD  17961  coafval  18061  efgval  19689  gsum2dlem1  19942  gsum2dlem2  19943  dprddomprc  19974  dprdval0prc  19976  psrvscafval  21915  mavmul0g  22504  mdetralt  22559  mdetunilem9  22571  cfinfil  23846  pcofval  24986  i1fima2  25657  i1fd  25659  itgeq2  25756  ibladdlem  25798  nbgrnself2  29250  clwwlknondisj  29998  nfrgr2v  30159  avril1  30350  nmobndseqi  30666  nonbooli  31538  chpssati  32250  nn0difffzod  32661  hashxpe  32664  1arithufdlem4  33364  hasheuni  33837  ddemeas  33988  bnj1143  34554  distel  35532  linedegen  35872  ordcmp  36064  bj-babygodel  36213  bj-nexrt  36302  bj-csbprc  36521  onsucuni3  36979  finxpnom  37013  wl-ifp-ncond1  37076  wl-ax11-lem8  37192  unccur  37209  matunitlindflem1  37222  poimirlem26  37252  poimirlem27  37253  poimirlem31  37257  cnambfre  37274  ibladdnclem  37282  frinfm  37341  tsbi3  37741  mopickr  37967  ax13fromc9  38510  axc711  38518  axc711toc7  38520  axc5c711toc7  38524  equidqe  38526  equidq  38528  ax12indalem  38549  hdmap1eulem  41427  hdmapevec  41440  intnanrt  41831  jm2.22  42560  clsk1indlem2  43616  nanorxor  43886  binomcxplemfrat  43932  binomcxplemradcnv  43933  pm10.251  43941  axc5c4c711toc7  43985  en3lpVD  44428  ax6e2ndeqVD  44492  2sb5ndVD  44493  ax6e2ndeqALT  44514  2sb5ndALT  44515  sineq0ALT  44520  nel1nelin  44654  nel2nelin  44655  axccdom  44736  fzdifsuc2  44832  liminf0  45321  cncfiooicc  45422  itgcoscmulx  45497  sge0sn  45907  isomenndlem  46058  hoidmvlelem2  46124  et-ltneverrefl  46399  singoutnword  46408  nabctnabc  46453  dfafv2  46652  afv2ndefb  46744  spr0el  46961  prmdvdsfmtnof1lem2  47064