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

Theorem con3i 149
Description: A contraposition inference. Inference associated with con3 148. Its associated inference is mto 187. (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 134 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  164  pm2.65i  184  pm5.21ni  366  pm2.45  411  pm2.46  412  pm5.14  926  con3ALT  1026  con3OLD  1029  rb-ax2  1669  rb-ax4  1671  ax13OLD  2293  sbequi  2363  euor2  2502  baroco  2560  necon3bi  2808  prcnel  3191  eueq3  3348  sbc2or  3411  sbcimdvOLD  3466  sbcrextOLD  3479  difrab  3860  csbprcOLD  3933  sbcel12  3935  sbcne12  3938  sbcel2  3941  ifeqor  4082  ifan  4084  nelpri  4149  nelprd  4151  eqoreldif  4172  opprc1  4363  opprc2  4364  snexALT  4778  mosubopt  4897  csbopab  4932  csbxp  5123  soirri  5441  predpoirr  5625  predfrirr  5626  nsuceq0  5722  csbiota  5797  nfvres  6134  fvco4i  6186  fvmptex  6203  fvopab4ndm  6215  ressnop0  6325  csbriota  6523  ovprc  6581  ovprc1  6582  ovprc2  6583  ndmovass  6720  ndmovdistr  6721  eldifpw  6868  nlimsucg  6934  tfindsg  6952  findsg  6985  curry1val  7157  curry2val  7161  extmptsuppeq  7206  funsssuppss  7208  eceqoveq  7740  fiprc  7924  sdomirr  7982  domtriord  7991  2pwuninel  8000  mapdom1  8010  nfielex  8074  relprcnfsupp  8161  supval2  8244  wemapso2  8341  card2inf  8343  en2lp  8393  wemapwe  8477  rankxplim3  8627  fidomtri2  8703  alephnbtwn  8777  kmlem2  8856  isfin7-2  9101  dominf  9150  ac6n  9190  alephval2  9273  dominfac  9274  axpowndlem3  9300  gchdomtri  9330  nlt1pi  9607  adderpq  9657  mulerpq  9658  zeo  11339  xrge0neqmnf  12147  fzoval  12340  bcpasc  12970  hashnemnf  12994  hasheq0  13015  hashunx  13036  hashbc  13094  flodddiv4lt  14977  prmreclem4  15461  ressinbas  15763  natfval  16429  fucbas  16443  fuchom  16444  arwval  16516  coafval  16537  grpidval  17083  symgbas  17623  efgval  17953  gsum2dlem1  18192  gsum2dlem2  18193  dprddomprc  18222  dprdval0prc  18224  psrvscafval  19211  mavmul0g  20178  mdetralt  20233  mdetunilem9  20245  tgdif0  20607  resstopn  20800  cfinfil  21507  pcofval  22618  i1fima2  23252  i1fd  23254  itgeq2  23350  ibladdlem  23392  cusgrafi  26010  uvtx01vtx  26020  frgra2v  26526  2spotiundisj  26589  numclwwlkdisj  26607  avril1  26711  nmobndseqi  27018  nonbooli  27894  chpssati  28606  hasheuni  29474  inelpisys  29544  ddemeas  29626  bnj1143  30115  rdgprc0  30943  distel  30953  linedegen  31420  ordcmp  31616  bj-babygodel  31761  bj-nexrt  31869  bj-csbprc  32096  bj-projval  32177  onsucuni3  32391  finxpnom  32414  wl-naev  32481  wl-hbnaev  32484  wl-ax11-lem8  32548  unccur  32562  matunitlindflem1  32575  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  cnambfre  32628  itg2addnclem3  32633  ibladdnclem  32636  frinfm  32700  tsbi3  33112  ax13fromc9  33209  axc711  33217  axc711toc7  33219  axc5c711toc7  33223  equidqe  33225  equidq  33227  ax12indalem  33248  hdmap1eulem  36131  hdmapevec  36145  jm2.22  36580  rp-fakeimass  36876  or3or  37339  clsk1indlem2  37360  nanorxor  37526  binomcxplemfrat  37572  binomcxplemradcnv  37573  pm10.251  37581  axc5c4c711toc7  37627  en3lpVD  38102  ax6e2ndeqVD  38167  2sb5ndVD  38168  ax6e2ndeqALT  38189  2sb5ndALT  38190  sineq0ALT  38195  axccdom  38411  fzdifsuc2  38466  cncfiooicc  38780  itgcoscmulx  38861  sge0sn  39272  iundjiunlem  39352  isomenndlem  39420  hoidmvlelem2  39486  smfmbfcex  39646  nabctnabc  39747  ndmafv  39869  nfunsnafv  39871  afvprc  39873  afvnufveq  39876  aovprc  39917  ndmaovass  39935  ndmaovdistr  39936  prmdvdsfmtnof1lem2  40035  clwwlksndisj  41280  nfrgr2v  41442  setrec2lem1  42239
  Copyright terms: Public domain W3C validator