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  367  pm2.45  412  pm2.46  413  pm5.14  929  con3ALT  1031  con3OLD  1034  rb-ax2  1676  rb-ax4  1678  ax13ALT  2303  sbequi  2373  euor2  2512  baroco  2570  necon3bi  2817  prcnel  3213  eueq3  3375  sbc2or  3438  sbcimdvOLD  3493  sbcrextOLD  3506  difrab  3893  csbprcOLD  3972  sbcel12  3974  sbcne12  3977  sbcel2  3980  ifeqor  4123  ifan  4125  nelpri  4192  nelprd  4194  eqoreldif  4216  opprc1  4416  opprc2  4417  snexALT  4843  mosubopt  4962  csbopab  4998  nprrel12  5150  csbxp  5190  soirri  5510  predpoirr  5696  predfrirr  5697  nsuceq0  5793  csbiota  5869  nfvres  6211  fvco4i  6263  fvmptex  6281  fvopab4ndm  6293  ressnop0  6405  csbriota  6608  ovprc  6668  ovprc1  6669  ovprc2  6670  ndmovass  6807  ndmovdistr  6808  eldifpw  6961  nlimsucg  7027  tfindsg  7045  findsg  7078  curry1val  7255  curry2val  7259  extmptsuppeq  7304  funsssuppss  7306  eceqoveq  7838  fiprc  8024  sdomirr  8082  domtriord  8091  2pwuninel  8100  mapdom1  8110  nfielex  8174  relprcnfsupp  8263  supval2  8346  wemapso2  8443  card2inf  8445  en2lp  8495  wemapwe  8579  rankxplim3  8729  fidomtri2  8805  alephnbtwn  8879  kmlem2  8958  isfin7-2  9203  dominf  9252  ac6n  9292  alephval2  9379  dominfac  9380  axpowndlem3  9406  gchdomtri  9436  nlt1pi  9713  adderpq  9763  mulerpq  9764  zeo  11448  xrge0neqmnf  12261  fzoval  12455  bcpasc  13091  hashnemnf  13115  hasheq0  13137  hashunx  13158  hashbc  13220  flodddiv4lt  15120  prmreclem4  15604  ressinbas  15917  natfval  16587  fucbas  16601  fuchom  16602  arwval  16674  coafval  16695  grpidval  17241  symgbas  17781  efgval  18111  gsum2dlem1  18350  gsum2dlem2  18351  dprddomprc  18380  dprdval0prc  18382  psrvscafval  19371  mavmul0g  20340  mdetralt  20395  mdetunilem9  20407  tgdif0  20777  resstopn  20971  cfinfil  21678  pcofval  22791  i1fima2  23427  i1fd  23429  itgeq2  23525  ibladdlem  23567  clwwlksndisj  26953  nfrgr2v  27116  avril1  27289  nmobndseqi  27604  nonbooli  28480  chpssati  29192  hasheuni  30121  inelpisys  30191  ddemeas  30273  bnj1143  30835  rdgprc0  31673  distel  31683  linedegen  32225  ordcmp  32421  bj-babygodel  32563  bj-nexrt  32657  bj-csbprc  32879  bj-projval  32959  onsucuni3  33186  finxpnom  33209  wl-naev  33273  wl-hbnaev  33276  wl-ax11-lem8  33340  unccur  33363  matunitlindflem1  33376  poimirlem26  33406  poimirlem27  33407  poimirlem31  33411  cnambfre  33429  itg2addnclem3  33434  ibladdnclem  33437  frinfm  33501  tsbi3  33913  ax13fromc9  34010  axc711  34018  axc711toc7  34020  axc5c711toc7  34024  equidqe  34026  equidq  34028  ax12indalem  34049  hdmap1eulem  36932  hdmapevec  36946  jm2.22  37381  rp-fakeimass  37676  or3or  38139  clsk1indlem2  38160  nanorxor  38324  binomcxplemfrat  38370  binomcxplemradcnv  38371  pm10.251  38379  axc5c4c711toc7  38425  en3lpVD  38900  ax6e2ndeqVD  38965  2sb5ndVD  38966  ax6e2ndeqALT  38987  2sb5ndALT  38988  sineq0ALT  38993  nel1nelin  39157  nel2nelin  39158  axccdom  39232  fzdifsuc2  39338  liminf0  39819  cncfiooicc  39870  itgcoscmulx  39948  sge0sn  40359  iundjiunlem  40439  isomenndlem  40507  hoidmvlelem2  40573  smfmbfcex  40731  nabctnabc  40861  ndmafv  40983  nfunsnafv  40985  afvnufveq  40990  aovprc  41031  ndmaovass  41049  ndmaovdistr  41050  prmdvdsfmtnof1lem2  41262  spr0el  41497  setrec2lem1  42205
  Copyright terms: Public domain W3C validator