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  1749  rb-ax4  1751  emptyex  1904  excomimw  2040  naev  2057  ax13ALT  2427  barocoALT  2674  necon3bi  2964  prcnel  3504  sbc2or  3799  difrab  4323  sbcel12  4416  sbcne12  4420  sbcel2  4423  rexn0  4516  ifeqor  4581  ifan  4583  nelpri  4659  nelprd  4661  eqoreldif  4689  snexALT  5388  csbopab  5564  nprrel12  5746  csbxp  5787  soirri  6148  predpoirr  6355  predfrirr  6356  nsuceq0  6468  csbiota  6555  eldifpw  7786  nlimsucg  7862  tfindsg  7881  findsg  7919  curry1val  8128  curry2val  8132  fsetdmprc0  8893  fiprc  9083  sdomirr  9152  domtriord  9161  2pwuninel  9170  mapdom1  9180  nfielex  9304  relprcnfsupp  9401  wemapso2  9590  card2inf  9592  en2lp  9643  wemapwe  9734  rankxplim3  9918  fidomtri2  10031  alephnbtwn  10108  kmlem2  10189  isfin7-2  10433  dominf  10482  ac6n  10522  alephval2  10609  dominfac  10610  gchdomtri  10666  nlt1pi  10943  zeo  12701  bcpasc  14356  hashnemnf  14379  hasheq0  14398  hashunx  14421  hashbc  14488  pfxval0  14710  flodddiv4lt  16450  prmreclem4  16952  ressinbas  17290  natfval  18000  fucbas  18015  fuchom  18016  fuchomOLD  18017  coafval  18117  efgval  19749  gsum2dlem1  20002  gsum2dlem2  20003  dprddomprc  20034  dprdval0prc  20036  psrvscafval  21985  mavmul0g  22574  mdetralt  22629  mdetunilem9  22641  cfinfil  23916  pcofval  25056  i1fima2  25727  i1fd  25729  itgeq2  25827  ibladdlem  25869  nbgrnself2  29391  clwwlknondisj  30139  nfrgr2v  30300  avril1  30491  nmobndseqi  30807  nonbooli  31679  chpssati  32391  nn0difffzod  32813  hashxpe  32816  gsumfs2d  33040  1arithufdlem4  33554  hasheuni  34065  ddemeas  34216  bnj1143  34782  distel  35784  linedegen  36124  ordcmp  36429  bj-babygodel  36585  bj-nexrt  36674  bj-csbprc  36892  onsucuni3  37349  finxpnom  37383  wl-ifp-ncond1  37446  wl-ax11-lem8  37572  unccur  37589  matunitlindflem1  37602  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  cnambfre  37654  ibladdnclem  37662  frinfm  37721  tsbi3  38121  mopickr  38344  ax13fromc9  38887  axc711  38895  axc711toc7  38897  axc5c711toc7  38901  equidqe  38903  equidq  38905  ax12indalem  38926  hdmap1eulem  41804  hdmapevec  41817  intnanrt  42224  jm2.22  42983  clsk1indlem2  44031  nanorxor  44300  binomcxplemfrat  44346  binomcxplemradcnv  44347  pm10.251  44355  axc5c4c711toc7  44399  en3lpVD  44842  ax6e2ndeqVD  44906  2sb5ndVD  44907  ax6e2ndeqALT  44928  2sb5ndALT  44929  sineq0ALT  44934  nel1nelin  45085  nel2nelin  45086  axccdom  45164  fzdifsuc2  45260  liminf0  45748  cncfiooicc  45849  itgcoscmulx  45924  sge0sn  46334  isomenndlem  46485  hoidmvlelem2  46551  et-ltneverrefl  46826  singoutnword  46835  nabctnabc  46880  dfafv2  47081  afv2ndefb  47173  spr0el  47406  prmdvdsfmtnof1lem2  47509