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

Theorem con1bii 322
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 283 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 302 . 2  |-  ( ph  <->  -. 
ps )
43bicomi 194 1  |-  ( -. 
ps 
<-> 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  con2bii  323  xor  862  3oran  953  had0  1409  mpto2OLD  1541  necon1abii  2618  necon1bbii  2619  npss  3417  dfnul3  3591  snprc  3831  dffv2  5755  kmlem3  7988  axpowndlem3  8430  nnunb  10173  rpnnen2  12780  ntreq0  17096  largei  23723  ballotlem2  24699  dffr5  25324  symdifass  25585  brsset  25643  brtxpsd  25648  tfrqfree  25704  dsmmacl  27075  pm10.252  27424  pm10.253  27425  2nexaln  27441  2exanali  27454  elpadd0  30291
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator