Metamath Proof Explorer


Theorem preqsnd

Description: Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016) (Revised by AV, 13-Jun-2022) (Revised by AV, 16-Aug-2024)

Ref Expression
Hypotheses preqsnd.1 φ A V
preqsnd.2 φ B W
Assertion preqsnd φ A B = C A = C B = C

Proof

Step Hyp Ref Expression
1 preqsnd.1 φ A V
2 preqsnd.2 φ B W
3 1 adantl C V φ A V
4 2 adantl C V φ B W
5 simpl C V φ C V
6 dfsn2 C = C C
7 6 eqeq2i A B = C A B = C C
8 preq12bg A V B W C V C V A B = C C A = C B = C A = C B = C
9 oridm A = C B = C A = C B = C A = C B = C
10 8 9 bitrdi A V B W C V C V A B = C C A = C B = C
11 7 10 syl5bb A V B W C V C V A B = C A = C B = C
12 3 4 5 5 11 syl22anc C V φ A B = C A = C B = C
13 snprc ¬ C V C =
14 13 biimpi ¬ C V C =
15 14 adantr ¬ C V φ C =
16 15 eqeq2d ¬ C V φ A B = C A B =
17 prnzg A V A B
18 eqneqall A B = A B A = C B = C
19 17 18 syl5com A V A B = A = C B = C
20 1 19 syl φ A B = A = C B = C
21 20 adantl ¬ C V φ A B = A = C B = C
22 16 21 sylbid ¬ C V φ A B = C A = C B = C
23 eleq1 C = A C V A V
24 23 eqcoms A = C C V A V
25 24 notbid A = C ¬ C V ¬ A V
26 pm2.24 A V ¬ A V B = C A B = C
27 elex A V A V
28 26 27 syl11 ¬ A V A V B = C A B = C
29 25 28 syl6bi A = C ¬ C V A V B = C A B = C
30 29 com13 A V ¬ C V A = C B = C A B = C
31 1 30 syl φ ¬ C V A = C B = C A B = C
32 31 impcom ¬ C V φ A = C B = C A B = C
33 32 impd ¬ C V φ A = C B = C A B = C
34 22 33 impbid ¬ C V φ A B = C A = C B = C
35 12 34 pm2.61ian φ A B = C A = C B = C