Theorem con3i 152

Description: A contraposition inference. Inference associated with con3 151. Its associated inference is mto 189. (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 138	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:  pm2.51  167  pm2.65i  186  pm5.21ni  370  pm2.45  865  pm2.46  866  pm5.14  929  con3ALT  1065  con3ALTOLD  1066  rb-ax2  1716  rb-ax4  1718  naev  2009  ax13ALT  2361  sbequiOLD  2455  sbequiALT  2523  euor2  2646  barocoALT  2712  necon3bi  2993  prcnel  3439  eueq3  3616  sbc2or  3690  difrab  4164  sbcel12  4246  sbcne12  4250  sbcel2  4253  ifeqor  4399  ifan  4401  nelpri  4466  nelprd  4468  eqoreldif  4496  opprc1  4701  opprc2  4702  snexALT  5136  mosubopt  5256  csbopab  5294  nprrel12  5460  csbxp  5500  soirri  5826  predpoirr  6014  predfrirr  6015  nsuceq0  6109  csbiota  6181  nfvres  6536  fvco4i  6589  fvmptex  6608  fvopab4ndm  6622  ressnop0  6738  csbriota  6949  ovprc  7013  ovprc1  7014  ovprc2  7015  ndmovass  7152  ndmovdistr  7153  eldifpw  7307  nlimsucg  7373  tfindsg  7391  findsg  7424  curry1val  7608  curry2val  7612  extmptsuppeq  7657  funsssuppss  7659  eceqoveq  8202  fiprc  8392  sdomirr  8450  domtriord  8459  2pwuninel  8468  mapdom1  8478  nfielex  8542  relprcnfsupp  8631  supval2  8714  wemapso2  8812  card2inf  8814  en2lp  8864  wemapwe  8954  rankxplim3  9104  fidomtri2  9217  alephnbtwn  9291  kmlem2  9371  isfin7-2  9616  dominf  9665  ac6n  9705  alephval2  9792  dominfac  9793  axpowndlem3  9819  gchdomtri  9849  nlt1pi  10126  adderpq  10176  mulerpq  10177  zeo  11881  fzoval  12855  bcpasc  13496  hashnemnf  13519  hasheq0  13539  hashunx  13560  hashbc  13624  swrdnznd  13805  pfxval0  13858  pfxnd0  13870  flodddiv4lt  15626  prmreclem4  16111  ressinbas  16416  natfval  17074  fucbas  17088  fuchom  17089  coafval  17182  grpidval  17728  symgbas  18269  efgval  18601  gsum2dlem1  18843  gsum2dlem2  18844  dprddomprc  18872  dprdval0prc  18874  psrvscafval  19884  mavmul0g  20866  mdetralt  20921  mdetunilem9  20933  tgdif0  21304  resstopn  21498  cfinfil  22205  pcofval  23317  i1fima2  23983  i1fd  23985  itgeq2  24081  ibladdlem  24123  nbgrnself2  26845  clwwlknondisj  27639  nfrgr2v  27806  avril1  28019  nmobndseqi  28333  nonbooli  29209  chpssati  29921  hashxpe  30283  hasheuni  30994  inelpisys  31064  ddemeas  31146  bnj1143  31716  rdgprc0  32565  distel  32575  linedegen  33131  ordcmp  33321  bj-babygodel  33460  bj-nexrt  33542  bj-csbprc  33724  bj-projval  33832  onsucuni3  34096  finxpnom  34129  wl-nax6al  34206  wl-ax11-lem8  34271  unccur  34322  matunitlindflem1  34335  poimirlem26  34365  poimirlem27  34366  poimirlem31  34370  cnambfre  34387  itg2addnclem3  34392  ibladdnclem  34395  frinfm  34458  tsbi3  34863  ax13fromc9  35493  axc711  35501  axc711toc7  35503  axc5c711toc7  35507  equidqe  35509  equidq  35511  ax12indalem  35532  hdmap1eulem  38409  hdmapevec  38422  jm2.22  38994  rp-fakeimass  39280  or3or  39740  clsk1indlem2  39761  nanorxor  40059  binomcxplemfrat  40105  binomcxplemradcnv  40106  pm10.251  40114  axc5c4c711toc7  40159  en3lpVD  40604  ax6e2ndeqVD  40668  2sb5ndVD  40669  ax6e2ndeqALT  40690  2sb5ndALT  40691  sineq0ALT  40696  nel1nelin  40843  nel2nelin  40844  axccdom  40918  fzdifsuc2  41012  liminf0  41511  cncfiooicc  41613  itgcoscmulx  41690  sge0sn  42098  iundjiunlem  42178  isomenndlem  42249  hoidmvlelem2  42315  smfmbfcex  42473  nabctnabc  42603  dfafv2  42743  ndmafv  42751  nfunsnafv  42753  afvnufveq  42758  aovprc  42799  ndmaovass  42817  ndmaovdistr  42818  afv2ndefb  42835  tz6.12-2-afv2  42848  spr0el  43018  prmdvdsfmtnof1lem2  43121  setrec2lem1  44169