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

Theorem notbii 627
Description: Negate both sides of a logical equivalence. (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 id 19 . . 3 ((𝜑𝜓) → (𝜑𝜓))
32notbid 625 . 2 ((𝜑𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
41, 3ax-mp 7 1 𝜑 ↔ ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sylnbi  636  xchnxbi  638  xchbinx  640  dcbii  783  xorcom  1322  xordidc  1333  sbn  1871  neirr  2260  dfrex2dc  2367  ddifstab  3121  dfss4st  3221  ssddif  3222  difin  3225  difundi  3240  difindiss  3242  indifdir  3244  rabeq0  3301  abeq0  3302  snprc  3489  difprsnss  3557  uni0b  3660  brdif  3867  unidif0  3975  dtruex  4346  dcextest  4367  difopab  4535  cnvdif  4800  imadiflem  5054  imadif  5055  brprcneu  5254  poxp  5947  finexdc  6563  snexxph  6601  infmoti  6659  prltlu  6982  recexprlemdisj  7125  axpre-apti  7356  dfinfre  8344  fzdifsuc  9417  fzp1nel  9440  nndc  11090  nnti  11321
  Copyright terms: Public domain W3C validator