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  1412  mpto2OLD  1544  necon1abii  2644  necon1bbii  2645  npss  3444  dfnul3  3618  snprc  3858  dffv2  5782  kmlem3  8016  axpowndlem3  8458  nnunb  10201  rpnnen2  12808  ntreq0  17124  largei  23753  ballotlem2  24729  dffr5  25360  symdifass  25621  brsset  25679  brtxpsd  25684  tfrqfree  25741  dfint3  25742  dsmmacl  27117  pm10.252  27466  pm10.253  27467  2nexaln  27483  2exanali  27496  elpadd0  30337
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