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

Theorem con3i 150
Description: A contraposition inference. Inference associated with con3 149. 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 135 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  165  pm2.65i  185  pm5.21ni  366  pm2.45  411  pm2.46  412  pm5.14  948  con3ALT  1052  rb-ax2  1718  rb-ax4  1720  ax13ALT  2341  sbequi  2403  euor2  2543  baroco  2601  necon3bi  2849  prcnel  3249  eueq3  3414  sbc2or  3477  sbcimdvOLD  3532  sbcrextOLD  3545  difrab  3934  csbprcOLD  4014  sbcel12  4016  sbcne12  4019  sbcel2  4022  ifeqor  4165  ifan  4167  nelpri  4234  nelprd  4236  eqoreldif  4257  opprc1  4457  opprc2  4458  snexALT  4882  mosubopt  5001  csbopab  5037  nprrel12  5194  csbxp  5234  soirri  5557  predpoirr  5746  predfrirr  5747  nsuceq0  5843  csbiota  5919  nfvres  6262  fvco4i  6315  fvmptex  6333  fvopab4ndm  6346  ressnop0  6460  csbriota  6663  ovprc  6723  ovprc1  6724  ovprc2  6725  ndmovass  6864  ndmovdistr  6865  eldifpw  7018  nlimsucg  7084  tfindsg  7102  findsg  7135  curry1val  7315  curry2val  7319  extmptsuppeq  7364  funsssuppss  7366  eceqoveq  7895  fiprc  8080  sdomirr  8138  domtriord  8147  2pwuninel  8156  mapdom1  8166  nfielex  8230  relprcnfsupp  8319  supval2  8402  wemapso2  8499  card2inf  8501  en2lp  8548  wemapwe  8632  rankxplim3  8782  fidomtri2  8858  alephnbtwn  8932  kmlem2  9011  isfin7-2  9256  dominf  9305  ac6n  9345  alephval2  9432  dominfac  9433  axpowndlem3  9459  gchdomtri  9489  nlt1pi  9766  adderpq  9816  mulerpq  9817  zeo  11501  xrge0neqmnf  12314  fzoval  12510  bcpasc  13148  hashnemnf  13172  hasheq0  13192  hashunx  13213  hashbc  13275  flodddiv4lt  15186  prmreclem4  15670  ressinbas  15983  natfval  16653  fucbas  16667  fuchom  16668  arwval  16740  coafval  16761  grpidval  17307  symgbas  17846  efgval  18176  gsum2dlem1  18415  gsum2dlem2  18416  dprddomprc  18445  dprdval0prc  18447  psrvscafval  19438  mavmul0g  20407  mdetralt  20462  mdetunilem9  20474  tgdif0  20844  resstopn  21038  cfinfil  21744  pcofval  22856  i1fima2  23491  i1fd  23493  itgeq2  23589  ibladdlem  23631  nbgrnself2  26301  clwwlknondisj  27086  clwwlknondisjOLD  27090  nfrgr2v  27252  avril1  27449  nmobndseqi  27762  nonbooli  28638  chpssati  29350  hasheuni  30275  inelpisys  30345  ddemeas  30427  bnj1143  30987  rdgprc0  31823  distel  31833  linedegen  32375  ordcmp  32571  bj-babygodel  32713  bj-nexrt  32807  bj-csbprc  33029  bj-projval  33109  onsucuni3  33345  finxpnom  33368  wl-naev  33432  wl-hbnaev  33435  wl-ax11-lem8  33499  unccur  33522  matunitlindflem1  33535  poimirlem26  33565  poimirlem27  33566  poimirlem31  33570  cnambfre  33588  itg2addnclem3  33593  ibladdnclem  33596  frinfm  33660  tsbi3  34072  ax13fromc9  34510  axc711  34518  axc711toc7  34520  axc5c711toc7  34524  equidqe  34526  equidq  34528  ax12indalem  34549  hdmap1eulem  37430  hdmapevec  37444  jm2.22  37879  rp-fakeimass  38174  or3or  38636  clsk1indlem2  38657  nanorxor  38821  binomcxplemfrat  38867  binomcxplemradcnv  38868  pm10.251  38876  axc5c4c711toc7  38922  en3lpVD  39394  ax6e2ndeqVD  39459  2sb5ndVD  39460  ax6e2ndeqALT  39481  2sb5ndALT  39482  sineq0ALT  39487  nel1nelin  39651  nel2nelin  39652  axccdom  39730  fzdifsuc2  39838  liminf0  40343  cncfiooicc  40425  itgcoscmulx  40503  sge0sn  40914  iundjiunlem  40994  isomenndlem  41065  hoidmvlelem2  41131  smfmbfcex  41289  nabctnabc  41419  ndmafv  41541  nfunsnafv  41543  afvnufveq  41548  aovprc  41589  ndmaovass  41607  ndmaovdistr  41608  prmdvdsfmtnof1lem2  41822  spr0el  42057  setrec2lem1  42765
  Copyright terms: Public domain W3C validator