Theorem con3i 155

Description: A contraposition inference. Inference associated with con3 154. Its associated inference is mto 200. (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 23	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con3i.a	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl 141	1 ⊢ (¬ 𝜓 → ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  conax1  171  pm2.65iOLD  197  pm5.21ni  380  pm2.45  895  pm2.46  896  con3ALT  1101  rb-ax2  1786  rb-ax4  1788  emptyex  1940  excomimw  2077  naev  2095  ax13ALT  2459  barocoALT  2706  necon3bi  2986  prcnel  3482  sbc2or  3755  nel1nelin  4160  nel2nelin  4161  difrab  4271  sbcel12  4376  sbcne12  4380  sbcel2  4383  rexn0  4459  ifeqor  4541  ifan  4543  nelpri  4623  nelprd  4625  eqoreldif  4653  vneqv  5281  snexALT  5356  csbopab  5542  nprrel12  5721  csbxp  5764  soirri  6128  predpoirr  6338  predfrirr  6339  nsuceq0  6450  csbiota  6533  eldifpw  7773  nlimsucg  7844  tfindsg  7863  findsg  7900  curry1val  8106  curry2val  8110  fsetdmprc0  8858  fiprc  9048  sdomirr  9109  domtriord  9118  2pwuninel  9127  mapdom1  9137  nfielex  9241  relprcnfsupp  9331  wemapso2  9522  card2inf  9524  en2lp  9582  wemapwe  9673  rankxplim3  9860  fidomtri2  9996  alephnbtwn  10071  kmlem2  10151  isfin7-2  10395  dominf  10444  ac6n  10484  alephval2  10572  dominfac  10573  gchdomtri  10629  nlt1pi  10906  indval0  12237  zeo  12698  bcpasc  14375  hashnemnf  14398  hasheq0  14417  hashunx  14440  hashbc  14508  pfxval0  14736  flodddiv4lt  16497  prmreclem4  17001  ressinbas  17327  natfval  18028  fucbas  18042  fuchom  18043  coafval  18143  efgval  19831  gsum2dlem1  20084  gsum2dlem2  20085  dprddomprc  20116  dprdval0prc  20118  isfieldidl  21436  psrvscafval  22148  mavmul0g  22760  mdetralt  22815  mdetunilem9  22827  cfinfil  24101  pcofval  25220  i1fima2  25889  i1fd  25891  itgeq2  25988  ibladdlem  26030  nbgrnself2  29768  clwwlknondisj  30529  nfrgr2v  30694  avril1  30885  nmobndseqi  31202  nonbooli  32074  chpssati  32786  nn0difffzod  33219  hashxpe  33222  gsumfs2d  33445  1arithufdlem4  33901  hasheuni  34539  ddemeas  34691  bnj1143  35243  fineqvnttrclse  35594  fineqvinfep  35595  kardval  35622  kard0b  35629  distel  36330  linedegen  36672  ordcmp  37015  bj-babygodel  37253  bj-nexrt  37374  bj-csbprc  37602  onsucuni3  38070  finxpnom  38104  wl-ifp-ncond1  38167  unccur  38311  matunitlindflem1  38324  poimirlem26  38354  poimirlem27  38355  poimirlem31  38359  cnambfre  38376  ibladdnclem  38384  frinfm  38444  tsbi3  38842  mopickr  39078  ax13fromc9  39738  axc711  39746  axc711toc7  39748  axc5c711toc7  39752  equidqe  39754  equidq  39756  ax12indalem  39777  hdmap1eulem  42654  hdmapevec  42667  intnanrt  43033  jm2.22  43780  clsk1indlem2  44826  nanorxor  45073  binomcxplemfrat  45119  binomcxplemradcnv  45120  pm10.251  45128  axc5c4c711toc7  45172  en3lpVD  45611  ax6e2ndeqVD  45675  2sb5ndVD  45676  ax6e2ndeqALT  45697  2sb5ndALT  45698  sineq0ALT  45703  axccdom  45996  fzdifsuc2  46087  liminf0  46565  cncfiooicc  46666  itgcoscmulx  46741  sge0sn  47151  isomenndlem  47302  hoidmvlelem2  47368  et-ltneverrefl  47643  quantgodelALT  47647  nabctnabc  47726  dfafv2  47927  afv2ndefb  48019  spr0el  48289  prmdvdsfmtnof1lem2  48395  fucofvalne  50160