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

Theorem con1bii 346
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 304 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 324 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 214 1 𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  con2bii  347  xor  934  3oran  1055  2nexaln  1754  nnel  2902  npss  3695  symdifass  3831  dfnul3  3894  snprc  4223  dffv2  6228  kmlem3  8918  axpowndlem3  9365  nnunb  11232  rpnnen2lem12  14879  dsmmacl  20004  ntreq0  20791  largei  28972  spc2d  29159  ballotlem2  30328  dffr5  31348  brsset  31635  brtxpsd  31640  dfrecs2  31696  dfint3  31698  con1bii2  32808  notbinot1  33507  elpadd0  34572  pm10.252  38039  pm10.253  38040  2exanali  38066
  Copyright terms: Public domain W3C validator