Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2i Unicode version

Theorem con2i 120
 Description: A contraposition inference. Its associated inference is mt2 179. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
Hypothesis
Ref Expression
con2i.a
Assertion
Ref Expression
con2i

Proof of Theorem con2i
StepHypRef Expression
1 con2i.a . 2
2 id 22 . 2
31, 2nsyl3 119 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4 This theorem is referenced by:  nsyl  121  notnot1  122  pm2.65i  173  pm3.14  502  pclem6  930  hba1w  1814  axc4  1860  hba1-o  2228  festino  2404  calemes  2414  fresison  2416  calemos  2417  fesapo  2418  necon3ai  2685  necon2ai  2692  necon2bi  2694  necon4aiOLD  2696  neneqadOLD  2766  eueq3  3274  ssnpss  3606  psstr  3607  elndif  3627  n0i  3789  axnulALT  4579  nfcvb  4682  zfpair  4689  onssneli  4992  onxpdisj  5088  funtpg  5643  ftpg  6081  nlimsucg  6677  reldmtpos  6982  bren2  7566  sdom0  7669  domunsn  7687  sdom1  7739  enp1i  7775  alephval3  8512  dfac2  8532  cdainflem  8592  ackbij1lem18  8638  isfin4-3  8716  fincssdom  8724  fin23lem41  8753  fin45  8793  fin17  8795  fin1a2lem7  8807  axcclem  8858  pwcfsdom  8979  canthp1lem1  9051  hargch  9072  winainflem  9092  ltxrlt  9676  xmullem2  11486  rexmul  11492  xlemul1a  11509  fzdisj  11741  pmtrdifellem4  16504  psgnunilem3  16521  frgpcyg  18612  dvlog2lem  23033  lgsval2lem  23581  isusgra0  24347  usgraop  24350  cusgrares  24472  2pthlem2  24598  2spot0  25064  strlem1  27169  chrelat2i  27284  dfrdg4  29600  finminlem  30136  stoweidlem14  31796  alneu  32206  2nodd  32500  bj-nimn  34143  hlrelat2  35127  cdleme50ldil  36274 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
 Copyright terms: Public domain W3C validator