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

Theorem con1bii 333
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 293 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 312 . 2  |-  ( ph  <->  -. 
ps )
43bicomi 206 1  |-  ( -. 
ps 
<-> 
ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188
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 189
This theorem is referenced by:  con2bii  334  xor  902  3oran  1004  2nexaln  1702  nnel  2733  npss  3543  symdifass  3672  dfnul3  3734  snprc  4035  dffv2  5938  kmlem3  8582  axpowndlem3  9024  nnunb  10865  rpnnen2  14278  dsmmacl  19304  ntreq0  20093  largei  27920  spc2d  28107  ballotlem2  29321  dffr5  30393  brsset  30656  brtxpsd  30661  dfrecs2  30717  dfint3  30719  con1bii2  31734  notbinot1  32312  elpadd0  33374  pm10.252  36710  pm10.253  36711  2exanali  36737
  Copyright terms: Public domain W3C validator