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

Theorem con1bii 329
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 289 . . 3  |-  ( ph  <->  -. 
-.  ph )
2 con1bii.1 . . 3  |-  ( -. 
ph 
<->  ps )
31, 2xchbinx 308 . 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  330  xor  889  3oran  990  had0  1475  2nexaln  1656  necon1abiiOLD  2717  necon1bbiiOLD  2719  nnel  2799  npss  3600  symdifass  3724  dfnul3  3786  snprc  4079  dffv2  5921  kmlem3  8523  axpowndlem3  8965  nnunb  10787  rpnnen2  14043  dsmmacl  18945  ntreq0  19745  largei  27384  spc2d  27571  ballotlem2  28691  dffr5  29423  brsset  29767  brtxpsd  29772  tfrqfree  29829  dfint3  29830  notbinot1  30716  pm10.252  31507  pm10.253  31508  2exanali  31534  elpadd0  35930
  Copyright terms: Public domain W3C validator