MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con1bii 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 5    <-> wb 178
This theorem is referenced by:  con2bii  324  xor  866  3oran  956  had0  1399  mpto2  1529  necon1abii  2463  necon1bbii  2464  npss  3203  dfnul3  3365  snprc  3599  dffv2  5444  kmlem3  7662  axpowndlem3  8101  nnunb  9840  rpnnen2  12378  ntreq0  16646  largei  22677  dffr5  23280  symdifass  23546  brsset  23604  brtxpsd  23609  tfrqfree  23663  notev  24155  notal  24156  dsmmacl  26373  pm10.252  26722  pm10.253  26723  2nexaln  26739  2exanali  26752  elpadd0  28687
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator