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

Theorem con2i 136
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 135 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  137  notnot  138  pm2.65i  185  pm3.14  970  pclem6  1007  hba1w  2131  hba1wOLD  2132  axc4  2294  festino  2720  calemes  2730  fresison  2732  calemos  2733  fesapo  2734  necon3ai  2968  necon2ai  2972  necon2bi  2973  eueq3  3534  ssnpss  3861  psstr  3862  elndif  3886  n0i  4069  axnulALT  4922  nfcvb  5027  zfpair  5033  onxpdisj  5991  ftpg  6567  nlimsucg  7190  reldmtpos  7513  bren2  8141  sdom0  8249  domunsn  8267  sdom1  8317  enp1i  8352  alephval3  9134  dfac2OLD  9156  cdainflem  9216  ackbij1lem18  9262  isfin4-3  9340  fincssdom  9348  fin23lem41  9377  fin45  9417  fin17  9419  fin1a2lem7  9431  axcclem  9482  pwcfsdom  9608  canthp1lem1  9677  hargch  9698  winainflem  9718  ltxrlt  10311  xmullem2  12301  rexmul  12307  xlemul1a  12324  fzdisj  12576  lcmfunsnlem2lem2  15561  pmtrdifellem4  18107  psgnunilem3  18124  frgpcyg  20138  dvlog2lem  24620  lgsval2lem  25254  strlem1  29450  chrelat2i  29565  dfrdg4  32396  finminlem  32650  bj-nimn  32889  bj-modald  32999  finxpreclem3  33568  finxpreclem5  33570  hba1-o  34706  hlrelat2  35212  cdleme50ldil  36358  or3or  38846  stoweidlem14  40749  alneu  41722  2nodd  42341  elsetrecslem  42974
  Copyright terms: Public domain W3C validator