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  24110  symdifass  24371  brsset  24429  brtxpsd  24434  tfrqfree  24489  notev  24990  notal  24991  dsmmacl  27207  pm10.252  27556  pm10.253  27557  2nexaln  27573  2exanali  27586  elpadd0  29998
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