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

Theorem con1i 143
Description: A contraposition inference. Inference associated with con1 142. Its associated inference is mt3 191. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.)
Hypothesis
Ref Expression
con1i.1 𝜑𝜓)
Assertion
Ref Expression
con1i 𝜓𝜑)

Proof of Theorem con1i
StepHypRef Expression
1 id 22 . 2 𝜓 → ¬ 𝜓)
2 con1i.1 . 2 𝜑𝜓)
31, 2nsyl2 141 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:  pm2.24i  145  nsyl4  155  impi  159  simplim  162  pm3.13  521  nbior  901  pm5.55  937  rb-ax2  1669  rb-ax3  1670  rb-ax4  1671  spimfw  1865  hba1w  1961  hba1wOLD  1962  hbe1a  2009  sp  2041  axc4  2115  exmoeu  2490  moanim  2517  moexex  2529  necon1bi  2810  fvrn0  6126  nfunsn  6135  mpt2xneldm  7225  mpt2xopxnop0  7228  ixpprc  7815  fineqv  8060  unbndrank  8588  pf1rcl  19534  wlkntrllem3  26091  stri  28500  hstri  28508  ddemeas  29626  hbntg  30955  bj-modalb  31893  wl-nf-nf2  32463  hba1-o  33200  axc5c711  33221  naecoms-o  33230  axc5c4c711  37624  hbntal  37790
  Copyright terms: Public domain W3C validator