Metamath Proof Explorer

Theorem nelprd

Description: If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018)

Ref Expression
Hypotheses nelprd.1 φ A B
nelprd.2 φ A C
Assertion nelprd φ ¬ A B C


Step Hyp Ref Expression
1 nelprd.1 φ A B
2 nelprd.2 φ A C
3 neanior A B A C ¬ A = B A = C
4 elpri A B C A = B A = C
5 4 con3i ¬ A = B A = C ¬ A B C
6 3 5 sylbi A B A C ¬ A B C
7 1 2 6 syl2anc φ ¬ A B C