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, 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 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  881  3oran  979  had0  1450  2nexaln  1626  necon1abii  2660  necon1bbii  2661  npss  3463  dfnul3  3637  snprc  3936  dffv2  5761  kmlem3  8317  axpowndlem3  8760  axpowndlem3OLD  8761  nnunb  10571  rpnnen2  13504  dsmmacl  18125  ntreq0  18640  largei  25606  spc2d  25793  ballotlem2  26801  dffr5  27492  symdifass  27787  brsset  27849  brtxpsd  27854  tfrqfree  27911  dfint3  27912  notbinot1  28804  pm10.252  29538  pm10.253  29539  2exanali  29565  elpadd0  33175
  Copyright terms: Public domain W3C validator