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

Theorem notbii 594
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 592 . 2 ((𝜑𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
41, 3ax-mp 7 1 𝜑 ↔ ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  sylnbi  603  xchnxbi  605  xchbinx  607  dcbii  747  xorcom  1279  xordidc  1290  sbn  1826  neirr  2213  ssddif  3168  difin  3171  difundi  3186  difindiss  3188  indifdir  3190  rabeq0  3244  abeq0  3245  snprc  3432  difprsnss  3499  uni0b  3602  brdif  3809  unidif0  3917  dtruex  4268  difopab  4447  cnvdif  4708  imadiflem  4956  imadif  4957  brprcneu  5149  poxp  5831  prltlu  6557  recexprlemdisj  6700  axpre-apti  6931  fzdifsuc  8901  fzp1nel  8924  nndc  9764
  Copyright terms: Public domain W3C validator