Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > eqcomi | GIF version |
Description: Commutativity of equality. |
Ref | Expression |
---|---|
eqcomi.1 | ⊢ A:α |
eqcomi.2 | ⊢ R⊧[A = B] |
Ref | Expression |
---|---|
eqcomi | ⊢ R⊧[B = A] |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | weq 38 | . 2 ⊢ = :(α → (α → ∗)) | |
2 | eqcomi.1 | . . 3 ⊢ A:α | |
3 | eqcomi.2 | . . 3 ⊢ R⊧[A = B] | |
4 | 2, 3 | eqtypi 69 | . 2 ⊢ B:α |
5 | 1, 2, 4, 3 | dfov1 66 | . . 3 ⊢ R⊧(( = A)B) |
6 | 2, 4, 5 | eqcomx 47 | . 2 ⊢ R⊧(( = B)A) |
7 | 1, 4, 2, 6 | dfov2 67 | 1 ⊢ R⊧[B = A] |
Colors of variables: type var term |
Syntax hints: = ke 7 [kbr 9 ⊧wffMMJ2 11 wffMMJ2t 12 |
This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-refl 39 ax-eqmp 42 ax-ceq 46 |
This theorem depends on definitions: df-ov 65 |
This theorem is referenced by: mpbir 77 3eqtr4i 86 3eqtr3i 87 hbth 99 alrimiv 141 dfan2 144 hbct 145 olc 154 orc 155 exlimdv 157 cbvf 167 alrimi 170 exlimd 171 exmid 186 exnal 188 ax8 198 ax9 199 ax10 200 |
Copyright terms: Public domain | W3C validator |