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

Theorem con1bii 322
Description: A contraposition inference. (Contributed by NM, 5-Aug-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 283 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 302 . 2  |-  ( ph  <->  -. 
ps )
43bicomi 194 1  |-  ( -. 
ps 
<-> 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  con2bii  323  xor  862  3oran  953  had0  1409  mpto2OLD  1541  necon1abii  2601  necon1bbii  2602  npss  3400  dfnul3  3574  snprc  3814  dffv2  5735  kmlem3  7965  axpowndlem3  8407  nnunb  10149  rpnnen2  12752  ntreq0  17064  largei  23618  ballotlem2  24525  dffr5  25134  symdifass  25395  brsset  25453  brtxpsd  25458  tfrqfree  25514  dsmmacl  26876  pm10.252  27225  pm10.253  27226  2nexaln  27242  2exanali  27255  elpadd0  29923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator