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

Theorem notbii 642
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 640 . 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 588  ax-in2 589
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylnbi  652  xchnxbi  654  xchbinx  656  nndc  821  xorcom  1351  xordidc  1362  sbn  1903  neirr  2294  dfrex2dc  2405  ddifstab  3178  dfss4st  3279  ssddif  3280  difin  3283  difundi  3298  difindiss  3300  indifdir  3302  rabeq0  3362  abeq0  3363  snprc  3558  difprsnss  3628  uni0b  3731  disjnim  3890  brdif  3951  unidif0  4061  dtruex  4444  dcextest  4465  difopab  4642  cnvdif  4915  imadiflem  5172  imadif  5173  brprcneu  5382  poxp  6097  finexdc  6764  snexxph  6806  infmoti  6883  ismkvnex  6997  prltlu  7263  recexprlemdisj  7406  axpre-apti  7661  dfinfre  8682  fzdifsuc  9829  fzp1nel  9852  ntreq0  12228  bj-nnor  12873  bj-nndcALT  12890  nnti  13118
  Copyright terms: Public domain W3C validator