Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  con3i Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 id 22 . 2 𝜓 → ¬ 𝜓)
2 con3i.a . 2 (𝜑𝜓)
31, 2nsyl 137 1 𝜓 → ¬ 𝜑)
 Colors of variables: wff setvar class 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  366  pm2.45  866  pm2.46  867  pm5.14  929  con3ALT  1069  rb-ax2  1826  rb-ax4  1828  ax13ALT  2461  sbequi  2522  euor2  2663  baroco  2721  necon3bi  2969  prcnel  3370  eueq3  3533  sbc2or  3596  difrab  4049  csbprcOLD  4125  sbcel12  4127  sbcne12  4130  sbcel2  4133  ifeqor  4271  ifan  4273  nelpri  4340  nelprd  4342  eqoreldif  4363  opprc1  4563  opprc2  4564  snexALT  4983  mosubopt  5103  csbopab  5141  nprrel12  5300  csbxp  5340  soirri  5663  predpoirr  5851  predfrirr  5852  nsuceq0  5948  csbiota  6024  nfvres  6365  fvco4i  6418  fvmptex  6436  fvopab4ndm  6449  ressnop0  6563  csbriota  6766  ovprc  6828  ovprc1  6829  ovprc2  6830  ndmovass  6969  ndmovdistr  6970  eldifpw  7123  nlimsucg  7189  tfindsg  7207  findsg  7240  curry1val  7421  curry2val  7425  extmptsuppeq  7470  funsssuppss  7473  eceqoveq  8005  fiprc  8195  sdomirr  8253  domtriord  8262  2pwuninel  8271  mapdom1  8281  nfielex  8345  relprcnfsupp  8434  supval2  8517  wemapso2  8614  card2inf  8616  en2lp  8666  wemapwe  8758  rankxplim3  8908  fidomtri2  9020  alephnbtwn  9094  kmlem2  9175  isfin7-2  9420  dominf  9469  ac6n  9509  alephval2  9596  dominfac  9597  axpowndlem3  9623  gchdomtri  9653  nlt1pi  9930  adderpq  9980  mulerpq  9981  zeo  11665  xrge0neqmnfOLD  12483  fzoval  12679  bcpasc  13312  hashnemnf  13336  hasheq0  13356  hashunx  13377  hashbc  13439  flodddiv4lt  15347  prmreclem4  15830  ressinbas  16143  natfval  16813  fucbas  16827  fuchom  16828  arwval  16900  coafval  16921  grpidval  17468  symgbas  18007  efgval  18337  gsum2dlem1  18576  gsum2dlem2  18577  dprddomprc  18607  dprdval0prc  18609  psrvscafval  19605  mavmul0g  20577  mdetralt  20632  mdetunilem9  20644  tgdif0  21017  resstopn  21211  cfinfil  21917  pcofval  23029  i1fima2  23666  i1fd  23668  itgeq2  23764  ibladdlem  23806  nbgrnself2  26479  clwwlknondisj  27287  clwwlknondisjOLD  27292  nfrgr2v  27454  avril1  27661  nmobndseqi  27974  nonbooli  28850  chpssati  29562  hasheuni  30487  inelpisys  30557  ddemeas  30639  bnj1143  31199  rdgprc0  32035  distel  32045  linedegen  32587  ordcmp  32783  bj-babygodel  32925  bj-nexrt  33019  bj-csbprc  33233  bj-projval  33315  onsucuni3  33552  finxpnom  33575  wl-naev  33639  wl-hbnaev  33642  wl-ax11-lem8  33703  unccur  33725  matunitlindflem1  33738  poimirlem26  33768  poimirlem27  33769  poimirlem31  33773  cnambfre  33790  itg2addnclem3  33795  ibladdnclem  33798  frinfm  33862  tsbi3  34274  ax13fromc9  34714  axc711  34722  axc711toc7  34724  axc5c711toc7  34728  equidqe  34730  equidq  34732  ax12indalem  34753  hdmap1eulem  37632  hdmapevec  37645  jm2.22  38088  rp-fakeimass  38383  or3or  38845  clsk1indlem2  38866  nanorxor  39030  binomcxplemfrat  39076  binomcxplemradcnv  39077  pm10.251  39085  axc5c4c711toc7  39131  en3lpVD  39602  ax6e2ndeqVD  39667  2sb5ndVD  39668  ax6e2ndeqALT  39689  2sb5ndALT  39690  sineq0ALT  39695  nel1nelin  39857  nel2nelin  39858  axccdom  39934  fzdifsuc2  40041  liminf0  40543  cncfiooicc  40625  itgcoscmulx  40702  sge0sn  41113  iundjiunlem  41193  isomenndlem  41264  hoidmvlelem2  41330  smfmbfcex  41488  nabctnabc  41618  ndmafv  41740  nfunsnafv  41742  afvnufveq  41747  aovprc  41788  ndmaovass  41806  ndmaovdistr  41807  prmdvdsfmtnof1lem2  42025  spr0el  42260  setrec2lem1  42968
 Copyright terms: Public domain W3C validator