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

Theorem con1i 129
Description: A contraposition inference. Its associated inference is mt3 180. (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.a
Assertion
Ref Expression
con1i

Proof of Theorem con1i
StepHypRef Expression
1 id 22 . 2
2 con1i.a . 2
31, 2nsyl2 127 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  nsyl4  142  pm2.24i  144  impi  148  simplim  151  pm3.13  501  nbior  860  pm5.55  897  rb-ax2  1586  rb-ax3  1587  rb-ax4  1588  spimfw  1737  hba1w  1814  sp  1859  axc4  1860  hba1-o  2228  axc5c711  2248  naecoms-o  2257  exmoeu  2316  moanim  2350  moexex  2363  necon3biOLD  2687  necon1aiOLD  2689  necon1bi  2690  fvrn0  5893  nfunsn  5902  mpt2xopxnop0  6962  ixpprc  7510  fineqv  7755  unbndrank  8281  pf1rcl  18385  wlkntrllem3  24563  stri  27176  hstri  27184  ddemeas  28208  hbntg  29238  axc5c4c711  31308  hbntal  33326  bj-naecomsv  34318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator