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

Theorem con1i 149
Description: A contraposition inference. Inference associated with con1 148. Its associated inference is mt3 202. (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 143 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  153  nsyl4  161  impi  165  simplim  168  nbior  881  pm5.55  942  pm3.13  988  rb-ax2  1745  rb-ax3  1746  rb-ax4  1747  spimfw  1959  hba1w  2045  hbe1a  2139  sp  2172  axc4  2331  exmoeu  2659  moanimlem  2696  moexexlem  2704  necon1bi  3041  fvrn0  6691  nfunsn  6700  mpoxneldm  7867  mpoxopxnop0  7870  ixpprc  8471  fineqv  8721  unbndrank  9259  pf1rcl  20440  stri  29961  hstri  29969  ddemeas  31394  hbntg  32947  bj-modalb  33947  wl-nax6im  34640  hba1-o  35913  axc5c711  35934  naecoms-o  35943  axc5c4c711  40610  hbntal  40764
  Copyright terms: Public domain W3C validator