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

Theorem con1i 147
Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 200. (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  150  nsyl4  158  nsyl5  159  impi  164  simplim  167  nbior  885  pm3.13  992  rb-ax2  1747  rb-ax3  1748  rb-ax4  1749  spimfw  1961  hba1w  2042  hbe1a  2132  sp  2171  axc4  2309  exmoeu  2569  necon1bi  2958  fvrn0  6926  nfunsn  6938  mpoxneldm  8218  mpoxopxnop0  8221  ixpprc  8938  fineqv  9288  unbndrank  9867  pf1rcl  22293  stri  32139  hstri  32147  ddemeas  33983  hbntg  35529  bj-modalb  36321  hba1-o  38496  axc5c711  38517  naecoms-o  38526  nfa1w  42232  axc5c4c711  43977  hbntal  44131
  Copyright terms: Public domain W3C validator