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  3044  prcnel  3520  eueq3  3704  sbc2or  3783  difrab  4279  sbcel12  4362  sbcne12  4366  sbcel2  4369  ifeqor  4518  ifan  4520  nelpri  4596  nelprd  4598  eqoreldif  4624  opprc1  4829  opprc2  4830  snexALT  5286  mosubopt  5402  csbopab  5444  nprrel12  5612  csbxp  5652  soirri  5988  predpoirr  6178  predfrirr  6179  nsuceq0  6273  csbiota  6350  nfvres  6708  fvco4i  6764  fvmptex  6784  fvopab4ndm  6799  ressnop0  6917  csbriota  7131  ovprc  7196  ovprc1  7197  ovprc2  7198  ndmovass  7338  ndmovdistr  7339  eldifpw  7492  nlimsucg  7559  tfindsg  7577  findsg  7611  curry1val  7802  curry2val  7806  extmptsuppeq  7856  funsssuppss  7858  eceqoveq  8404  fiprc  8597  sdomirr  8656  domtriord  8665  2pwuninel  8674  mapdom1  8684  nfielex  8749  relprcnfsupp  8838  supval2  8921  wemapso2  9019  card2inf  9021  en2lp  9071  wemapwe  9162  rankxplim3  9312  fidomtri2  9425  alephnbtwn  9499  kmlem2  9579  isfin7-2  9820  dominf  9869  ac6n  9909  alephval2  9996  dominfac  9997  axpowndlem3  10023  gchdomtri  10053  nlt1pi  10330  adderpq  10380  mulerpq  10381  zeo  12071  fzoval  13042  bcpasc  13684  hashnemnf  13707  hasheq0  13727  hashunx  13750  hashbc  13814  swrdnznd  14006  pfxval0  14040  pfxnd0  14052  flodddiv4lt  15768  prmreclem4  16257  ressinbas  16562  natfval  17218  fucbas  17232  fuchom  17233  coafval  17326  grpidval  17873  efgval  18845  gsum2dlem1  19092  gsum2dlem2  19093  dprddomprc  19124  dprdval0prc  19126  psrvscafval  20172  mavmul0g  21164  mdetralt  21219  mdetunilem9  21231  tgdif0  21602  resstopn  21796  cfinfil  22503  pcofval  23616  i1fima2  24282  i1fd  24284  itgeq2  24380  ibladdlem  24422  nbgrnself2  27144  clwwlknondisj  27892  nfrgr2v  28053  avril1  28244  nmobndseqi  28558  nonbooli  29430  chpssati  30142  hashxpe  30531  hasheuni  31346  inelpisys  31415  ddemeas  31497  bnj1143  32064  rdgprc0  33040  distel  33050  linedegen  33606  ordcmp  33797  bj-babygodel  33939  bj-nexrt  34028  bj-csbprc  34228  bj-projval  34310  onsucuni3  34650  finxpnom  34684  wl-ax11-lem8  34826  unccur  34877  matunitlindflem1  34890  poimirlem26  34920  poimirlem27  34921  poimirlem31  34925  cnambfre  34942  itg2addnclem3  34947  ibladdnclem  34950  frinfm  35012  tsbi3  35415  ax13fromc9  36044  axc711  36052  axc711toc7  36054  axc5c711toc7  36058  equidqe  36060  equidq  36062  ax12indalem  36083  hdmap1eulem  38960  hdmapevec  38973  jm2.22  39599  or3or  40378  clsk1indlem2  40399  nanorxor  40644  binomcxplemfrat  40690  binomcxplemradcnv  40691  pm10.251  40699  axc5c4c711toc7  40743  en3lpVD  41186  ax6e2ndeqVD  41250  2sb5ndVD  41251  ax6e2ndeqALT  41272  2sb5ndALT  41273  sineq0ALT  41278  nel1nelin  41422  nel2nelin  41423  axccdom  41494  fzdifsuc2  41584  liminf0  42081  cncfiooicc  42184  itgcoscmulx  42261  sge0sn  42668  iundjiunlem  42748  isomenndlem  42819  hoidmvlelem2  42885  smfmbfcex  43043  nabctnabc  43174  dfafv2  43338  ndmafv  43346  nfunsnafv  43348  afvnufveq  43353  aovprc  43394  ndmaovass  43412  ndmaovdistr  43413  afv2ndefb  43430  tz6.12-2-afv2  43443  spr0el  43651  prmdvdsfmtnof1lem2  43754  setrec2lem1  44803