![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > notbii | GIF version |
Description: Negate both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
notbii.1 | ⊢ (φ ↔ ψ) |
Ref | Expression |
---|---|
notbii | ⊢ (¬ φ ↔ ¬ ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notbii.1 | . 2 ⊢ (φ ↔ ψ) | |
2 | id 19 | . . 3 ⊢ ((φ ↔ ψ) → (φ ↔ ψ)) | |
3 | 2 | notbid 591 | . 2 ⊢ ((φ ↔ ψ) → (¬ φ ↔ ¬ ψ)) |
4 | 1, 3 | ax-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 602 xchnxbi 604 xchbinx 606 dcbii 746 xorcom 1276 xordidc 1287 sbn 1823 neirr 2210 ssddif 3165 difin 3168 difundi 3183 difindiss 3185 indifdir 3187 rabeq0 3241 abeq0 3242 snprc 3426 difprsnss 3493 uni0b 3596 brdif 3803 unidif0 3911 dtruex 4237 difopab 4412 cnvdif 4673 imadiflem 4921 imadif 4922 brprcneu 5114 poxp 5794 prltlu 6470 recexprlemdisj 6602 axpre-apti 6769 fzdifsuc 8713 fzp1nel 8736 nndc 9235 |
Copyright terms: Public domain | W3C validator |