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

Theorem con1bii 345
 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 303 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 323 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 213 1 𝜓𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195 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 196 This theorem is referenced by:  con2bii  346  xor  931  3oran  1050  2nexaln  1747  nnel  2892  npss  3679  symdifass  3815  dfnul3  3877  snprc  4197  dffv2  6181  kmlem3  8857  axpowndlem3  9300  nnunb  11165  rpnnen2lem12  14793  dsmmacl  19904  ntreq0  20691  largei  28510  spc2d  28697  ballotlem2  29877  dffr5  30896  brsset  31166  brtxpsd  31171  dfrecs2  31227  dfint3  31229  con1bii2  32355  notbinot1  33048  elpadd0  34113  pm10.252  37582  pm10.253  37583  2exanali  37609
 Copyright terms: Public domain W3C validator