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

Theorem con1i 132
Description: A contraposition inference. Inference associated with con1 131. Its associated inference is mt3 183. (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  |-  ( -. 
ph  ->  ps )
Assertion
Ref Expression
con1i  |-  ( -. 
ps  ->  ph )

Proof of Theorem con1i
StepHypRef Expression
1 id 22 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con1i.1 . 2  |-  ( -. 
ph  ->  ps )
31, 2nsyl2 130 1  |-  ( -. 
ps  ->  ph )
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  136  nsyl4  147  impi  151  simplim  154  pm3.13  503  nbior  868  pm5.55  905  rb-ax2  1630  rb-ax3  1631  rb-ax4  1632  spimfw  1788  hba1w  1868  sp  1914  axc4  1915  exmoeu  2303  moanim  2330  moexex  2342  necon1bi  2624  fvrn0  5842  nfunsn  5851  mpt2xneldm  6908  mpt2xopxnop0  6911  ixpprc  7493  fineqv  7735  unbndrank  8260  pf1rcl  18875  wlkntrllem3  25228  stri  27847  hstri  27855  ddemeas  29006  hbntg  30398  bj-naecomsv  31258  hba1-o  32381  axc5c711  32401  naecoms-o  32410  axc5c4c711  36665  hbntal  36833
  Copyright terms: Public domain W3C validator