![]() |
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 2112 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | |
4 | 1, 2, 3 | syl2an 285 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1299 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-4 1455 ax-17 1474 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-cleq 2093 |
This theorem is referenced by: eqeqan12rd 2116 eqfnfv 5450 eqfnfv2 5451 f1mpt 5604 xpopth 6004 f1o2ndf1 6055 ecopoveq 6454 xpdom2 6654 djune 6878 addpipqqs 7079 enq0enq 7140 enq0sym 7141 enq0tr 7143 enq0breq 7145 preqlu 7181 cnegexlem1 7808 neg11 7884 subeqrev 8005 cnref1o 9290 xneg11 9458 modlteq 10011 sq11 10206 fz1eqb 10378 cj11 10518 sqrt11 10651 sqabs 10694 recan 10721 reeff1 11205 efieq 11240 tgtop11 12027 |
Copyright terms: Public domain | W3C validator |