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

Theorem notbii 604
 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 602 . 2 ((𝜑𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
41, 3ax-mp 7 1 𝜑 ↔ ¬ 𝜓)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  sylnbi  613  xchnxbi  615  xchbinx  617  dcbii  758  xorcom  1295  xordidc  1306  sbn  1842  neirr  2229  ssddif  3198  difin  3201  difundi  3216  difindiss  3218  indifdir  3220  rabeq0  3274  abeq0  3275  snprc  3462  difprsnss  3529  uni0b  3632  brdif  3839  unidif0  3947  dtruex  4310  difopab  4496  cnvdif  4757  imadiflem  5005  imadif  5006  brprcneu  5198  poxp  5880  prltlu  6642  recexprlemdisj  6785  axpre-apti  7016  fzdifsuc  9044  fzp1nel  9067  nndc  10266
 Copyright terms: Public domain W3C validator