Theorem con3i 157

Description: A contraposition inference. Inference associated with con3 156. Its associated inference is mto 199. (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 142	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  172  pm2.65i  196  pm5.21ni  381  pm2.45  878  pm2.46  879  con3ALT  1080  con3ALTOLD  1081  rb-ax2  1754  rb-ax4  1756  emptyex  1908  naev  2065  ax13ALT  2447  sbequiOLD  2534  sbequiALT  2596  euor2  2697  barocoALT  2762  necon3bi  3042  prcnel  3518  eueq3  3702  sbc2or  3781  difrab  4277  sbcel12  4360  sbcne12  4364  sbcel2  4367  ifeqor  4516  ifan  4518  nelpri  4594  nelprd  4596  eqoreldif  4622  opprc1  4827  opprc2  4828  snexALT  5284  mosubopt  5400  csbopab  5442  nprrel12  5610  csbxp  5650  soirri  5986  predpoirr  6176  predfrirr  6177  nsuceq0  6271  csbiota  6348  nfvres  6706  fvco4i  6762  fvmptex  6782  fvopab4ndm  6797  ressnop0  6915  csbriota  7129  ovprc  7194  ovprc1  7195  ovprc2  7196  ndmovass  7336  ndmovdistr  7337  eldifpw  7490  nlimsucg  7557  tfindsg  7575  findsg  7609  curry1val  7800  curry2val  7804  extmptsuppeq  7854  funsssuppss  7856  eceqoveq  8402  fiprc  8595  sdomirr  8654  domtriord  8663  2pwuninel  8672  mapdom1  8682  nfielex  8747  relprcnfsupp  8836  supval2  8919  wemapso2  9017  card2inf  9019  en2lp  9069  wemapwe  9160  rankxplim3  9310  fidomtri2  9423  alephnbtwn  9497  kmlem2  9577  isfin7-2  9818  dominf  9867  ac6n  9907  alephval2  9994  dominfac  9995  axpowndlem3  10021  gchdomtri  10051  nlt1pi  10328  adderpq  10378  mulerpq  10379  zeo  12069  fzoval  13040  bcpasc  13682  hashnemnf  13705  hasheq0  13725  hashunx  13748  hashbc  13812  swrdnznd  14004  pfxval0  14038  pfxnd0  14050  flodddiv4lt  15766  prmreclem4  16255  ressinbas  16560  natfval  17216  fucbas  17230  fuchom  17231  coafval  17324  grpidval  17871  efgval  18843  gsum2dlem1  19090  gsum2dlem2  19091  dprddomprc  19122  dprdval0prc  19124  psrvscafval  20170  mavmul0g  21162  mdetralt  21217  mdetunilem9  21229  tgdif0  21600  resstopn  21794  cfinfil  22501  pcofval  23614  i1fima2  24280  i1fd  24282  itgeq2  24378  ibladdlem  24420  nbgrnself2  27142  clwwlknondisj  27890  nfrgr2v  28051  avril1  28242  nmobndseqi  28556  nonbooli  29428  chpssati  30140  hashxpe  30529  hasheuni  31344  inelpisys  31413  ddemeas  31495  bnj1143  32062  rdgprc0  33038  distel  33048  linedegen  33604  ordcmp  33795  bj-babygodel  33937  bj-nexrt  34026  bj-csbprc  34229  bj-projval  34311  onsucuni3  34651  finxpnom  34685  wl-ax11-lem8  34839  unccur  34890  matunitlindflem1  34903  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  cnambfre  34955  itg2addnclem3  34960  ibladdnclem  34963  frinfm  35025  tsbi3  35428  ax13fromc9  36057  axc711  36065  axc711toc7  36067  axc5c711toc7  36071  equidqe  36073  equidq  36075  ax12indalem  36096  hdmap1eulem  38973  hdmapevec  38986  jm2.22  39612  or3or  40391  clsk1indlem2  40412  nanorxor  40657  binomcxplemfrat  40703  binomcxplemradcnv  40704  pm10.251  40712  axc5c4c711toc7  40756  en3lpVD  41199  ax6e2ndeqVD  41263  2sb5ndVD  41264  ax6e2ndeqALT  41285  2sb5ndALT  41286  sineq0ALT  41291  nel1nelin  41435  nel2nelin  41436  axccdom  41507  fzdifsuc2  41597  liminf0  42094  cncfiooicc  42197  itgcoscmulx  42274  sge0sn  42681  iundjiunlem  42761  isomenndlem  42832  hoidmvlelem2  42898  smfmbfcex  43056  nabctnabc  43187  dfafv2  43351  ndmafv  43359  nfunsnafv  43361  afvnufveq  43366  aovprc  43407  ndmaovass  43425  ndmaovdistr  43426  afv2ndefb  43443  tz6.12-2-afv2  43456  spr0el  43664  prmdvdsfmtnof1lem2  43767  setrec2lem1  44816