Com ., ∨, ⊕, ≡ (4 classes)
PA ., ∨, ⊕, ≡ (4 classes, bidirectional)
DC p∨q ↔ ~p⊃q
DC2 ~p∨q ↔ p⊃q
DM ~(p.q) ↔ ~p∨~q and ~(p∨q) ↔ ~p.~q
Dist ∨ over ., . over ∨ (bidirectional)
Rep p ↔ p∨p and p ↔ p.p
CT p⊃q ↔ ~q⊃~p and p≡q ↔ ~p≡~q
LB p≡q ↔ (p⊃q).(q⊃p)
DB p≡q ↔ (p.q)∨(~p.~q)
ED p⊕q ↔ (p∨q).(~p∨~q)
ME p⊕q ↔ ~(p≡q)
Exp (p.q)⊃r ↔ p⊃(q⊃r)
BA p⊃q ↔ p⊃(p.q)
To use the PME Rules, Select a line, Select 'Rewrite Rules' from the Rules Menu.