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 2152 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | |
4 | 1, 2, 3 | syl2an 287 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1331 |
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 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 |
This theorem is referenced by: eqeqan12rd 2156 eqfnfv 5518 eqfnfv2 5519 f1mpt 5672 xpopth 6074 f1o2ndf1 6125 ecopoveq 6524 xpdom2 6725 djune 6963 addpipqqs 7178 enq0enq 7239 enq0sym 7240 enq0tr 7242 enq0breq 7244 preqlu 7280 cnegexlem1 7937 neg11 8013 subeqrev 8138 cnref1o 9440 xneg11 9617 modlteq 10170 sq11 10365 fz1eqb 10537 cj11 10677 sqrt11 10811 sqabs 10854 recan 10881 reeff1 11407 efieq 11442 tgtop11 12245 |
Copyright terms: Public domain | W3C validator |