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

Theorem con2i 120
Description: A contraposition inference. (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  921  hba1w  1754  axc4  1800  sbnOLD  2093  hba1-o  2208  festino  2401  calemes  2411  fresison  2413  calemos  2414  fesapo  2415  necon3ai  2681  necon2ai  2688  necon2bi  2690  necon4aiOLD  2692  neneqadOLD  2762  eueq3  3244  ssnpss  3573  psstr  3574  elndif  3594  n0i  3756  axnulALT  4536  nfcvb  4639  zfpair  4646  onssneli  4945  onxpdisj  5037  funtpg  5587  ftpg  6016  nlimsucg  6586  reldmtpos  6887  bren2  7474  sdom0  7577  domunsn  7595  sdom1  7647  enp1i  7682  alephval3  8417  dfac2  8437  cdainflem  8497  ackbij1lem18  8543  isfin4-3  8621  fincssdom  8629  fin23lem41  8658  fin45  8698  fin17  8700  fin1a2lem7  8712  axcclem  8763  pwcfsdom  8884  canthp1lem1  8956  hargch  8977  winainflem  8997  renfdisj  9574  ltxrlt  9582  xmullem2  11367  rexmul  11373  xlemul1a  11390  fzdisj  11621  pmtrdifellem4  16144  psgnunilem3  16161  frgpcyg  18199  dvlog2lem  22497  lgsval2lem  23045  isusgra0  23744  cusgrares  23849  2pthlem2  23964  strlem1  26123  chrelat2i  26238  dfrdg4  28437  finminlem  28973  stoweidlem14  30543  fourierswlem  30760  fouriersw  30761  alneu  30902  2spot0  31534  hlrelat2  33898  cdleme50ldil  35043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator