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

Theorem con2i 126
 Description: A contraposition inference. Its associated inference is mt2 186. (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 125 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  127  notnot  128  pm2.65i  180  pm3.14  516  pclem6  957  hba1w  1922  axc4  1991  festino  2454  calemes  2464  fresison  2466  calemos  2467  fesapo  2468  necon3ai  2702  necon2ai  2706  necon2bi  2707  eueq3  3237  ssnpss  3558  psstr  3559  elndif  3582  n0i  3762  axnulALT  4564  nfcvb  4671  zfpair  4678  onssneli  5583  onxpdisj  5593  funtpg  5684  ftpg  6142  nlimsucg  6746  reldmtpos  7058  bren2  7683  sdom0  7788  domunsn  7806  sdom1  7856  enp1i  7891  alephval3  8626  dfac2  8646  cdainflem  8706  ackbij1lem18  8752  isfin4-3  8830  fincssdom  8838  fin23lem41  8867  fin45  8907  fin17  8909  fin1a2lem7  8921  axcclem  8972  pwcfsdom  9093  canthp1lem1  9162  hargch  9183  winainflem  9203  ltxrlt  9789  xmullem2  11646  rexmul  11652  xlemul1a  11669  fzdisj  11922  lcmfunsnlem2lem2  14774  pmtrdifellem4  17281  psgnunilem3  17298  frgpcyg  19302  dvlog2lem  23758  lgsval2lem  24395  isusgra0  25235  usgraop  25238  cusgrares  25361  2pthlem2  25487  2spot0  25952  strlem1  28066  chrelat2i  28181  dfrdg4  30869  finminlem  31123  bj-nimn  31331  bj-modald  31454  finxpreclem3  32006  finxpreclem5  32008  hba1-o  32702  hlrelat2  33208  cdleme50ldil  34355  stoweidlem14  38310  alneu  39142  2nodd  41002
 Copyright terms: Public domain W3C validator