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

Theorem con1bii 340
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 notnotb 299 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 319 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 209 1 𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 191
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 192
This theorem is referenced by:  con2bii  341  xor  921  3oran  1040  2nexaln  1733  nnel  2787  npss  3565  symdifass  3699  dfnul3  3760  snprc  4064  dffv2  6005  kmlem3  8667  axpowndlem3  9109  nnunb  10956  rpnnen2  14438  dsmmacl  19462  ntreq0  20250  largei  28083  spc2d  28270  ballotlem2  29475  dffr5  30544  brsset  30807  brtxpsd  30812  dfrecs2  30868  dfint3  30870  con1bii2  31955  notbinot1  32549  elpadd0  33614  pm10.252  37067  pm10.253  37068  2exanali  37094
  Copyright terms: Public domain W3C validator