Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > equequ2 | GIF version |
Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
equequ2 | ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equtrr 1686 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | |
2 | equtrr 1686 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) | |
3 | 2 | equcoms 1684 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) |
4 | 1, 3 | impbid 128 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
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-gen 1425 ax-ie2 1470 ax-8 1482 ax-17 1506 ax-i9 1510 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v2 1792 ax11v 1799 ax11ev 1800 equs5or 1802 eujust 2001 euf 2004 mo23 2040 eleq1w 2200 disjiun 3924 iotaval 5099 dffun4f 5139 dff13f 5671 supmoti 6880 isoti 6894 ennnfonelemr 11936 ctinf 11943 |
Copyright terms: Public domain | W3C validator |