Metamath Proof Explorer
Description: A Tseitin axiom for logical exclusive disjunction, in deduction form.
(Contributed by Giovanni Mascellani, 24-Mar-2018)
|
|
Ref |
Expression |
|
Assertion |
tsxo1 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
tsbi1 |
|
2 |
|
xnor |
|
3 |
2
|
orbi2i |
|
4 |
1 3
|
sylib |
|