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  781  xorcom  1320  xordidc  1331  sbn  1869  neirr  2258  dfrex2dc  2365  ddifstab  3116  ssddif  3216  difin  3219  difundi  3234  difindiss  3236  indifdir  3238  rabeq0  3295  abeq0  3296  snprc  3481  difprsnss  3549  uni0b  3652  brdif  3859  unidif0  3967  dtruex  4338  dcextest  4359  difopab  4527  cnvdif  4792  imadiflem  5046  imadif  5047  brprcneu  5246  poxp  5932  finexdc  6545  snexxph  6583  infmoti  6630  prltlu  6949  recexprlemdisj  7092  axpre-apti  7323  dfinfre  8311  fzdifsuc  9388  fzp1nel  9411  nndc  11004  nnti  11234
  Copyright terms: Public domain W3C validator