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

Theorem con2i 114
 Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by 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 21 . 2
31, 2nsyl3 113 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6 This theorem is referenced by:  nsyl  115  notnot1  116  pm2.65i  167  pm3.14  490  pclem6  901  ax12o10lem4  1638  ax12o10lem5  1639  ax12o10lem8  1642  ax12olem23  1657  ax5o  1693  hba1  1718  19.8a  1758  a4ime  1868  sbn  1954  a4sbe  1967  festino  2218  calemes  2228  fresison  2230  calemos  2231  fesapo  2232  necon3ai  2452  necon2bi  2458  necon4ai  2471  neneqad  2482  eueq3  2877  ssnpss  3199  psstr  3200  elndif  3217  n0i  3367  nfcvb  4099  zfpair  4106  onssneli  4393  nlimsucg  4524  onxpdisj  4676  reldmtpos  6094  bren2  6778  sdom0  6878  domunsn  6896  sdom1  6947  enp1i  6978  alephval3  7621  dfac2  7641  cdainflem  7701  ackbij1lem18  7747  isfin4-3  7825  fincssdom  7833  fin23lem41  7862  fin45  7902  fin17  7904  fin1a2lem7  7916  axcclem  7967  pwcfsdom  8085  canthp1lem1  8154  hargch  8179  winainflem  8195  renfdisj  8765  ltxrlt  8773  xmullem2  10463  rexmul  10469  xlemul1a  10486  fzdisj  10695  frgpcyg  16359  dvlog2lem  19831  lgsval2lem  20377  strlem1  22660  chrelat2i  22775  axfelem18  23531  axfelem22  23535  dfrdg4  23662  finminlem  25397  psgnunilem3  26585  ax12-4  27795  ax12conj2  27797  a12study8  27808  a12study  27821  ax9lem7  27835  ax9lem12  27840  ax9lem15  27843  hlrelat2  28281  cdleme50ldil  29426 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
 Copyright terms: Public domain W3C validator