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 2177 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | |
4 | 1, 2, 3 | syl2an 287 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1342 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: eqeqan12rd 2181 eqfnfv 5577 eqfnfv2 5578 f1mpt 5733 xpopth 6136 f1o2ndf1 6187 ecopoveq 6587 xpdom2 6788 djune 7034 addpipqqs 7302 enq0enq 7363 enq0sym 7364 enq0tr 7366 enq0breq 7368 preqlu 7404 cnegexlem1 8064 neg11 8140 subeqrev 8265 cnref1o 9579 xneg11 9761 modlteq 10322 sq11 10517 fz1eqb 10693 cj11 10833 sqrt11 10967 sqabs 11010 recan 11037 reeff1 11627 efieq 11662 tgtop11 12623 ioocosf1o 13322 |
Copyright terms: Public domain | W3C validator |