![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr2di | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
eqtr2di.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eqtr2di.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqtr2di |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr2di.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqtr2di.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtrdi 2203 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | eqcomd 2160 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 1424 ax-gen 1426 ax-4 1487 ax-17 1503 ax-ext 2136 |
This theorem depends on definitions: df-bi 116 df-cleq 2147 |
This theorem is referenced by: eqtr4id 2206 elxp4 5066 elxp5 5067 fo1stresm 6099 fo2ndresm 6100 eloprabi 6134 fo2ndf 6164 xpsnen 6755 xpassen 6764 ac6sfi 6832 undifdc 6857 ine0 8248 nn0n0n1ge2 9213 fzval2 9893 fseq1p1m1 9974 fsum2dlemstep 11308 modfsummodlemstep 11331 fprod2dlemstep 11496 ef4p 11568 sin01bnd 11631 odd2np1 11737 sqpweven 12020 2sqpwodd 12021 psmetdmdm 12663 xmetdmdm 12695 dveflem 13026 reeff1oleme 13032 abssinper 13106 |
Copyright terms: Public domain | W3C validator |