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

Theorem con1bii 331
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypothesis
Ref Expression
con1bii.1  |-  ( -. 
ph 
<->  ps )
Assertion
Ref Expression
con1bii  |-  ( -. 
ps 
<-> 
ph )

Proof of Theorem con1bii
StepHypRef Expression
1 notnot 291 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 310 . 2  |-  ( ph  <->  -. 
ps )
43bicomi 202 1  |-  ( -. 
ps 
<-> 
ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  con2bii  332  xor  887  3oran  987  had0  1450  2nexaln  1626  necon1abiiOLD  2725  necon1bbiiOLD  2727  nnel  2807  npss  3609  dfnul3  3783  snprc  4086  dffv2  5933  kmlem3  8523  axpowndlem3  8966  axpowndlem3OLD  8967  nnunb  10782  rpnnen2  13811  dsmmacl  18534  ntreq0  19339  largei  26850  spc2d  27037  ballotlem2  28055  dffr5  28747  symdifass  29042  brsset  29104  brtxpsd  29109  tfrqfree  29166  dfint3  29167  notbinot1  30068  pm10.252  30801  pm10.253  30802  2exanali  30828  elpadd0  34482
  Copyright terms: Public domain W3C validator