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

Theorem con1bii 321
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 282 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 301 . 2  |-  ( ph  <->  -. 
ps )
43bicomi 193 1  |-  ( -. 
ps 
<-> 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  con2bii  322  xor  861  3oran  951  had0  1393  mpto2  1524  necon1abii  2497  necon1bbii  2498  npss  3286  dfnul3  3458  snprc  3695  dffv2  5592  kmlem3  7778  axpowndlem3  8221  nnunb  9961  rpnnen2  12504  ntreq0  16814  largei  22847  ballotlem2  23047  dffr5  23521  symdifass  23782  brsset  23840  brtxpsd  23845  tfrqfree  23900  notev  24402  notal  24403  dsmmacl  26619  pm10.252  26968  pm10.253  26969  2nexaln  26985  2exanali  26998  elpadd0  29371
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 177
  Copyright terms: Public domain W3C validator