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  mpto2OLD  1525  necon1abii  2510  necon1bbii  2511  npss  3299  dfnul3  3471  snprc  3708  dffv2  5608  kmlem3  7794  axpowndlem3  8237  nnunb  9977  rpnnen2  12520  ntreq0  16830  largei  22863  ballotlem2  23063  dffr5  24181  symdifass  24442  brsset  24500  brtxpsd  24505  tfrqfree  24561  notev  25093  notal  25094  dsmmacl  27310  pm10.252  27659  pm10.253  27660  2nexaln  27676  2exanali  27689  elpadd0  30620
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