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

Theorem con1bii 323
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 284 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 303 . 2  |-  ( ph  <->  -. 
ps )
43bicomi 195 1  |-  ( -. 
ps 
<-> 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178
This theorem is referenced by:  con2bii  324  xor  863  3oran  954  had0  1413  mpto2OLD  1545  necon1abii  2661  necon1bbii  2662  npss  3443  dfnul3  3616  snprc  3895  dffv2  5825  kmlem3  8063  axpowndlem3  8505  nnunb  10248  rpnnen2  12856  ntreq0  17172  largei  23801  ballotlem2  24777  dffr5  25407  symdifass  25703  brsset  25765  brtxpsd  25770  tfrqfree  25827  dfint3  25828  dsmmacl  27222  pm10.252  27571  pm10.253  27572  2nexaln  27588  2exanali  27601  elpadd0  30704
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 179
  Copyright terms: Public domain W3C validator