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

Theorem con2i 134
Description: A contraposition inference. Its associated inference is mt2 191. (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 133 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:  nsyl  135  notnot  136  pm2.65i  185  pm3.14  523  pclem6  970  hba1w  1971  hba1wOLD  1972  axc4  2126  festino  2570  calemes  2580  fresison  2582  calemos  2583  fesapo  2584  necon3ai  2815  necon2ai  2819  necon2bi  2820  eueq3  3368  ssnpss  3694  psstr  3695  elndif  3718  n0i  3902  axnulALT  4757  nfcvb  4868  zfpair  4875  onxpdisj  5816  funtpgOLD  5911  ftpg  6388  nlimsucg  7004  reldmtpos  7320  bren2  7946  sdom0  8052  domunsn  8070  sdom1  8120  enp1i  8155  alephval3  8893  dfac2  8913  cdainflem  8973  ackbij1lem18  9019  isfin4-3  9097  fincssdom  9105  fin23lem41  9134  fin45  9174  fin17  9176  fin1a2lem7  9188  axcclem  9239  pwcfsdom  9365  canthp1lem1  9434  hargch  9455  winainflem  9475  ltxrlt  10068  xmullem2  12054  rexmul  12060  xlemul1a  12077  fzdisj  12326  lcmfunsnlem2lem2  15295  pmtrdifellem4  17839  psgnunilem3  17856  frgpcyg  19862  dvlog2lem  24332  lgsval2lem  24966  strlem1  28997  chrelat2i  29112  dfrdg4  31753  finminlem  32007  bj-nimn  32246  bj-modald  32356  finxpreclem3  32901  finxpreclem5  32903  hba1-o  33701  hlrelat2  34208  cdleme50ldil  35355  or3or  37840  stoweidlem14  39568  alneu  40535  2nodd  41130  elsetrecslem  41767
  Copyright terms: Public domain W3C validator