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 193. (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 145 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  148  nsyl4  158  impi  162  simplim  165  nbior  874  pm5.55  934  pm3.13  980  rb-ax2  1797  rb-ax3  1798  rb-ax4  1799  spimfw  2009  hba1w  2092  hbe1a  2138  sp  2167  axc4  2296  exmoeu  2601  exmoeuOLD  2632  moanimlem  2653  moexex  2668  necon1bi  2997  fvrn0  6476  nfunsn  6486  mpt2xneldm  7622  mpt2xopxnop0  7625  ixpprc  8217  fineqv  8465  unbndrank  9004  pf1rcl  20113  stri  29692  hstri  29700  ddemeas  30901  hbntg  32303  bj-modalb  33298  wl-nax6im  33899  hba1-o  35056  axc5c711  35077  naecoms-o  35086  axc5c4c711  39567  hbntal  39723
  Copyright terms: Public domain W3C validator