Theorem con3i 151

Description: A contraposition inference. Inference associated with con3 150. Its associated inference is mto 188. (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 137	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  166  pm2.65i  185  pm5.21ni  368  pm2.45  897  pm2.46  898  pm5.14  960  con3ALT  1098  rb-ax2  1833  rb-ax4  1835  ax13ALT  2473  sbequi  2534  euor2  2677  barocoALT  2743  necon3bi  3004  prcnel  3412  eueq3  3579  sbc2or  3642  difrab  4102  sbcel12  4180  sbcne12  4183  sbcel2  4186  ifeqor  4328  ifan  4330  nelpri  4395  nelprd  4397  eqoreldif  4418  opprc1  4619  opprc2  4620  snexALT  5052  mosubopt  5165  csbopab  5203  nprrel12  5360  csbxp  5402  soirri  5733  predpoirr  5921  predfrirr  5922  nsuceq0  6018  csbiota  6094  nfvres  6444  fvco4i  6497  fvmptex  6515  fvopab4ndm  6528  ressnop0  6644  csbriota  6847  ovprc  6911  ovprc1  6912  ovprc2  6913  ndmovass  7052  ndmovdistr  7053  eldifpw  7206  nlimsucg  7272  tfindsg  7290  findsg  7323  curry1val  7504  curry2val  7508  extmptsuppeq  7553  funsssuppss  7556  eceqoveq  8088  fiprc  8278  sdomirr  8336  domtriord  8345  2pwuninel  8354  mapdom1  8364  nfielex  8428  relprcnfsupp  8517  supval2  8600  wemapso2  8697  card2inf  8699  en2lp  8749  wemapwe  8841  rankxplim3  8991  fidomtri2  9103  alephnbtwn  9177  kmlem2  9258  isfin7-2  9503  dominf  9552  ac6n  9592  alephval2  9679  dominfac  9680  axpowndlem3  9706  gchdomtri  9736  nlt1pi  10013  adderpq  10063  mulerpq  10064  zeo  11729  xrge0neqmnfOLD  12496  fzoval  12695  bcpasc  13328  hashnemnf  13352  hasheq0  13372  hashunx  13393  hashbc  13454  flodddiv4lt  15358  prmreclem4  15840  ressinbas  16147  natfval  16810  fucbas  16824  fuchom  16825  arwval  16897  coafval  16918  grpidval  17465  symgbas  18001  efgval  18331  gsum2dlem1  18570  gsum2dlem2  18571  dprddomprc  18601  dprdval0prc  18603  psrvscafval  19599  mavmul0g  20570  mdetralt  20625  mdetunilem9  20637  tgdif0  21010  resstopn  21204  cfinfil  21910  pcofval  23022  i1fima2  23660  i1fd  23662  itgeq2  23758  ibladdlem  23800  nbgrnself2  26472  clwwlknondisj  27280  clwwlknondisjOLD  27285  nfrgr2v  27447  avril1  27650  nmobndseqi  27962  nonbooli  28838  chpssati  29550  hasheuni  30472  inelpisys  30542  ddemeas  30624  bnj1143  31184  rdgprc0  32019  distel  32029  linedegen  32571  ordcmp  32763  bj-babygodel  32903  bj-nexrt  32997  bj-csbprc  33212  bj-projval  33294  onsucuni3  33531  finxpnom  33554  wl-naev  33618  wl-hbnaev  33621  wl-ax11-lem8  33683  unccur  33705  matunitlindflem1  33718  poimirlem26  33748  poimirlem27  33749  poimirlem31  33753  cnambfre  33770  itg2addnclem3  33775  ibladdnclem  33778  frinfm  33842  tsbi3  34252  ax13fromc9  34685  axc711  34693  axc711toc7  34695  axc5c711toc7  34699  equidqe  34701  equidq  34703  ax12indalem  34724  hdmap1eulem  37603  hdmapevec  37616  jm2.22  38063  rp-fakeimass  38357  or3or  38819  clsk1indlem2  38840  nanorxor  39004  binomcxplemfrat  39050  binomcxplemradcnv  39051  pm10.251  39059  axc5c4c711toc7  39104  en3lpVD  39574  ax6e2ndeqVD  39639  2sb5ndVD  39640  ax6e2ndeqALT  39661  2sb5ndALT  39662  sineq0ALT  39667  nel1nelin  39826  nel2nelin  39827  axccdom  39903  fzdifsuc2  40005  liminf0  40505  cncfiooicc  40587  itgcoscmulx  40664  sge0sn  41075  iundjiunlem  41155  isomenndlem  41226  hoidmvlelem2  41292  smfmbfcex  41450  nabctnabc  41580  dfafv2  41721  ndmafv  41729  nfunsnafv  41731  afvnufveq  41736  aovprc  41777  ndmaovass  41795  ndmaovdistr  41796  afv2ndefb  41813  tz6.12-2-afv2  41826  prmdvdsfmtnof1lem2  42072  spr0el  42300  setrec2lem1  43008