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  2472  necon1bbii  2473  npss  3261  dfnul3  3433  snprc  3669  dffv2  5526  kmlem3  7746  axpowndlem3  8189  nnunb  9928  rpnnen2  12466  ntreq0  16776  largei  22807  ballotlem2  23008  dffr5  23481  symdifass  23747  brsset  23805  brtxpsd  23810  tfrqfree  23864  notev  24356  notal  24357  dsmmacl  26574  pm10.252  26923  pm10.253  26924  2nexaln  26940  2exanali  26953  elpadd0  29165
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