![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeqan12d | GIF version |
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
eqeqan12d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqeqan12d.2 | ⊢ (𝜓 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
eqeqan12d | ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeqan12d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | eqeqan12d.2 | . 2 ⊢ (𝜓 → 𝐶 = 𝐷) | |
3 | eqeq12 2190 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | |
4 | 1, 2, 3 | syl2an 289 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: eqeqan12rd 2194 eqfnfv 5608 eqfnfv2 5609 f1mpt 5765 xpopth 6170 f1o2ndf1 6222 ecopoveq 6623 xpdom2 6824 djune 7070 addpipqqs 7347 enq0enq 7408 enq0sym 7409 enq0tr 7411 enq0breq 7413 preqlu 7449 cnegexlem1 8109 neg11 8185 subeqrev 8310 cnref1o 9626 xneg11 9808 modlteq 10370 sq11 10565 qsqeqor 10603 fz1eqb 10741 cj11 10885 sqrt11 11019 sqabs 11062 recan 11089 reeff1 11679 efieq 11714 ismhm 12730 tgtop11 13209 ioocosf1o 13908 |
Copyright terms: Public domain | W3C validator |