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  886  3oran  984  had0  1446  2nexaln  1622  necon1abiiOLD  2711  necon1bbiiOLD  2713  nnel  2793  npss  3564  dfnul3  3738  snprc  4037  dffv2  5863  kmlem3  8422  axpowndlem3  8865  axpowndlem3OLD  8866  nnunb  10676  rpnnen2  13610  dsmmacl  18275  ntreq0  18797  largei  25806  spc2d  25993  ballotlem2  27005  dffr5  27697  symdifass  27992  brsset  28054  brtxpsd  28059  tfrqfree  28116  dfint3  28117  notbinot1  29017  pm10.252  29751  pm10.253  29752  2exanali  29778  elpadd0  33759
  Copyright terms: Public domain W3C validator