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  863  3oran  953  had0  1395  mpto2  1525  necon1abii  2498  necon1bbii  2499  npss  3287  dfnul3  3459  snprc  3696  dffv2  5553  kmlem3  7773  axpowndlem3  8216  nnunb  9956  rpnnen2  12498  ntreq0  16808  largei  22839  ballotlem2  23040  dffr5  23513  symdifass  23779  brsset  23837  brtxpsd  23842  tfrqfree  23896  notev  24388  notal  24389  dsmmacl  26606  pm10.252  26955  pm10.253  26956  2nexaln  26972  2exanali  26985  elpadd0  29265
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