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

Theorem con2i 141
Description: A contraposition inference. Its associated inference is mt2 201. (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 140 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  142  notnot  144  pm2.65i  195  pm3.14  989  pclem6  1019  hba1w  2045  axc4  2331  festinoALT  2755  necon3ai  3038  necon2ai  3042  necon2bi  3043  eueq3  3699  ssnpss  4077  psstr  4078  elndif  4102  n0i  4296  axnulALT  5199  nfcvb  5268  zfpair  5312  epelg  5459  onxpdisj  6303  ftpg  6910  nlimsucg  7546  reldmtpos  7889  bren2  8528  sdom0  8637  domunsn  8655  sdom1  8706  enp1i  8741  alephval3  9524  cdainflem  9601  ackbij1lem18  9647  isfin4p1  9725  fincssdom  9733  fin23lem41  9762  fin17  9804  fin1a2lem7  9816  axcclem  9867  pwcfsdom  9993  canthp1lem1  10062  hargch  10083  winainflem  10103  ltxrlt  10699  xmullem2  12646  rexmul  12652  xlemul1a  12669  fzdisj  12922  lcmfunsnlem2lem2  15971  pmtrdifellem4  18536  psgnunilem3  18553  frgpcyg  20648  dvlog2lem  25162  lgsval2lem  25810  strlem1  29954  chrelat2i  30069  dfrdg4  33309  finminlem  33563  bj-nimn  33796  bj-modald  33903  finxpreclem3  34556  finxpreclem5  34558  hba1-o  35913  hlrelat2  36419  cdleme50ldil  37564  sn-dtru  38989  or3or  40249  stoweidlem14  42176  alneu  43200  2nodd  43956  smndex1n0mnd  44012  elsetrecslem  44729
  Copyright terms: Public domain W3C validator