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

Theorem con1bii 360
 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 318 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 337 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 227 1 𝜓𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209 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 210 This theorem is referenced by:  xor  1012  3anor  1105  3oran  1106  2nexaln  1831  2exanali  1861  nnel  3127  spc2d  3589  npss  4073  dfnul3  4279  snprc  4638  dffv2  6747  kmlem3  9576  axpowndlem3  10019  nnunb  11890  rpnnen2lem12  15578  dsmmacl  20437  ntreq0  21688  largei  30056  ballotlem2  31806  dffr5  33049  noetalem3  33279  brsset  33410  brtxpsd  33415  dfrecs2  33471  dfint3  33473  con1bii2  34697  notbinot1  35465  elpadd0  37053  pm10.252  40989  pm10.253  40990
 Copyright terms: Public domain W3C validator