# [SageMath], 140 bytes

<!-- language-all: lang-sagemath -->

    lambda p:propcalc.formula(r(r(r(r(r(p,"'","0"),"implies","->"),"or","|"),"and","&"),"not","~")).is_tautology()
    r=lambda s,a,b:s.replace(a,b)

[Try it online!](https://sagecell.sagemath.org/?z=eJx1UEsKwyAQ3XuKwUXjgA1dB9Iz5ACFYhJTBBNFzaJQevaOaUjTQp3FvHnvMR-H-sKsGttega98cL5TtisHF8bZKhG28JIXXPITR8nN6K3RkcrjOdcuEHxkpKae4CHDySWCT45YmnhNak7OuttdIAv1OjBKJdsqlkF7qzotqEKWdEwRahAM6HHRwDoOGuRyJfdsgRsmvtgJe6X54vHTqtl7XMj9_oh03K9KfrrzvRky-jXI64OZlhyrxeiDmZLIhIRhyYgvMrRp4A==&lang=sage&interacts=eJyLjgUAARUAuQ==)

[SageMath]: https://doc.sagemath.org/html/en/index.html