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

Theorem con1bii 344
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 302 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 322 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 212 1 𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194
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 195
This theorem is referenced by:  con2bii  345  xor  930  3oran  1049  2nexaln  1746  nnel  2891  npss  3678  symdifass  3814  dfnul3  3876  snprc  4196  dffv2  6166  kmlem3  8834  axpowndlem3  9277  nnunb  11135  rpnnen2lem12  14739  dsmmacl  19846  ntreq0  20633  largei  28316  spc2d  28503  ballotlem2  29683  dffr5  30702  brsset  30972  brtxpsd  30977  dfrecs2  31033  dfint3  31035  con1bii2  32151  notbinot1  32844  elpadd0  33909  pm10.252  37378  pm10.253  37379  2exanali  37405
  Copyright terms: Public domain W3C validator