MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con1bii 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
Assertion
Ref Expression
con1bii

Proof of Theorem con1bii
StepHypRef Expression
1 notnot 291 . . 3
2 con1bii.1 . . 3
31, 2xchbinx 310 . 2
43bicomi 202 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184
This theorem is referenced by:  con2bii  332  xor  891  3oran  992  had0  1471  2nexaln  1651  necon1abiiOLD  2720  necon1bbiiOLD  2722  nnel  2802  npss  3613  dfnul3  3787  snprc  4093  dffv2  5946  kmlem3  8553  axpowndlem3  8996  axpowndlem3OLD  8997  nnunb  10816  rpnnen2  13959  dsmmacl  18772  ntreq0  19578  largei  27186  spc2d  27373  ballotlem2  28427  dffr5  29182  symdifass  29477  brsset  29539  brtxpsd  29544  tfrqfree  29601  dfint3  29602  notbinot1  30476  pm10.252  31266  pm10.253  31267  2exanali  31293  elpadd0  35533
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
  Copyright terms: Public domain W3C validator