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  379  pm2.45  879  pm2.46  880  con3ALT  1084  rb-ax2  1760  rb-ax4  1762  emptyex  1914  naev  2067  ax13ALT  2427  barocoALT  2680  necon3bi  2972  prcnel  3454  sbc2or  3729  difrab  4248  sbcel12  4348  sbcne12  4352  sbcel2  4355  rexn0  4447  ifeqor  4516  ifan  4518  nelpri  4596  nelprd  4598  eqoreldif  4626  snexALT  5310  csbopab  5471  nprrel12  5646  csbxp  5686  soirri  6030  predpoirr  6235  predfrirr  6236  nsuceq0  6345  csbiota  6425  eldifpw  7612  nlimsucg  7683  tfindsg  7701  findsg  7740  curry1val  7936  curry2val  7940  fsetdmprc0  8626  fiprc  8818  sdomirr  8883  domtriord  8892  2pwuninel  8901  mapdom1  8911  nfielex  9025  relprcnfsupp  9109  wemapso2  9290  card2inf  9292  en2lp  9342  wemapwe  9433  rankxplim3  9640  fidomtri2  9753  alephnbtwn  9828  kmlem2  9908  isfin7-2  10153  dominf  10202  ac6n  10242  alephval2  10329  dominfac  10330  gchdomtri  10386  nlt1pi  10663  zeo  12406  bcpasc  14033  hashnemnf  14056  hasheq0  14076  hashunx  14099  hashbc  14163  pfxval0  14387  flodddiv4lt  16122  prmreclem4  16618  ressinbas  16953  natfval  17660  fucbas  17675  fuchom  17676  fuchomOLD  17677  coafval  17777  efgval  19321  gsum2dlem1  19569  gsum2dlem2  19570  dprddomprc  19601  dprdval0prc  19603  psrvscafval  21157  mavmul0g  21700  mdetralt  21755  mdetunilem9  21767  cfinfil  23042  pcofval  24171  i1fima2  24841  i1fd  24843  itgeq2  24940  ibladdlem  24982  nbgrnself2  27725  clwwlknondisj  28471  nfrgr2v  28632  avril1  28823  nmobndseqi  29137  nonbooli  30009  chpssati  30721  hashxpe  31123  hasheuni  32049  ddemeas  32200  bnj1143  32766  distel  33775  linedegen  34441  ordcmp  34632  bj-babygodel  34781  bj-nexrt  34870  bj-csbprc  35091  onsucuni3  35534  finxpnom  35568  wl-ifp-ncond1  35631  wl-ax11-lem8  35739  unccur  35756  matunitlindflem1  35769  poimirlem26  35799  poimirlem27  35800  poimirlem31  35804  cnambfre  35821  ibladdnclem  35829  frinfm  35889  tsbi3  36289  ax13fromc9  36916  axc711  36924  axc711toc7  36926  axc5c711toc7  36930  equidqe  36932  equidq  36934  ax12indalem  36955  hdmap1eulem  39832  hdmapevec  39845  jm2.22  40814  clsk1indlem2  41622  nanorxor  41893  binomcxplemfrat  41939  binomcxplemradcnv  41940  pm10.251  41948  axc5c4c711toc7  41992  en3lpVD  42435  ax6e2ndeqVD  42499  2sb5ndVD  42500  ax6e2ndeqALT  42521  2sb5ndALT  42522  sineq0ALT  42527  nel1nelin  42665  nel2nelin  42666  axccdom  42732  fzdifsuc2  42820  liminf0  43305  cncfiooicc  43406  itgcoscmulx  43481  sge0sn  43888  isomenndlem  44039  hoidmvlelem2  44105  nabctnabc  44394  dfafv2  44592  afv2ndefb  44684  spr0el  44903  prmdvdsfmtnof1lem2  45006