Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  notbii GIF version

Theorem notbii 657
 Description: Equivalence property for negation. Inference form. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
notbii.1 (𝜑𝜓)
Assertion
Ref Expression
notbii 𝜑 ↔ ¬ 𝜓)

Proof of Theorem notbii
StepHypRef Expression
1 notbii.1 . 2 (𝜑𝜓)
2 notbi 655 . 2 ((𝜑𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
31, 2ax-mp 5 1 𝜑 ↔ ¬ 𝜓)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  sylnbi  667  xchnxbi  669  xchbinx  671  nndc  836  xorcom  1366  xordidc  1377  sbn  1923  neirr  2315  dfrex2dc  2426  ddifstab  3203  dfss4st  3304  ssddif  3305  difin  3308  difundi  3323  difindiss  3325  indifdir  3327  rabeq0  3387  abeq0  3388  snprc  3583  difprsnss  3653  uni0b  3756  disjnim  3915  brdif  3976  unidif0  4086  dtruex  4469  dcextest  4490  difopab  4667  cnvdif  4940  imadiflem  5197  imadif  5198  brprcneu  5407  poxp  6122  finexdc  6789  snexxph  6831  infmoti  6908  ismkvnex  7022  prltlu  7288  recexprlemdisj  7431  axpre-apti  7686  dfinfre  8707  fzdifsuc  9854  fzp1nel  9877  ntreq0  12290  bj-nnor  12935  bj-nndcALT  12952  nnti  13180
 Copyright terms: Public domain W3C validator