MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con1bii Structured version   Unicode version

Theorem con1bii 331
Description: A contraposition inference. (Contributed by NM, 12-Mar-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 291 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 310 . 2  |-  ( ph  <->  -. 
ps )
43bicomi 202 1  |-  ( -. 
ps 
<-> 
ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  con2bii  332  xor  891  3oran  993  had0  1458  2nexaln  1638  necon1abiiOLD  2706  necon1bbiiOLD  2708  nnel  2788  npss  3599  dfnul3  3773  snprc  4078  dffv2  5931  kmlem3  8535  axpowndlem3  8978  axpowndlem3OLD  8979  nnunb  10797  rpnnen2  13836  dsmmacl  18645  ntreq0  19451  largei  27058  spc2d  27245  ballotlem2  28300  dffr5  29157  symdifass  29452  brsset  29514  brtxpsd  29519  tfrqfree  29576  dfint3  29577  notbinot1  30451  pm10.252  31220  pm10.253  31221  2exanali  31247  elpadd0  35273
  Copyright terms: Public domain W3C validator