![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr4id | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
eqtr4id.2 |
![]() ![]() ![]() ![]() |
eqtr4id.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqtr4id |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4id.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqtr4id.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | eqcomi 2158 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 3 | eqtr2di 2204 |
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: iftrue 3506 iffalse 3509 difprsn1 3691 dmmptg 5076 relcoi1 5110 funimacnv 5239 dmmptd 5293 dffv3g 5457 dfimafn 5510 fvco2 5530 isoini 5759 oprabco 6154 ixpconstg 6641 unfiexmid 6851 undifdc 6857 sbthlemi4 6893 sbthlemi5 6894 sbthlemi6 6895 supval2ti 6927 exmidfodomrlemim 7115 suplocexprlemex 7621 eqneg 8584 zeo 9248 fseq1p1m1 9974 seq3val 10335 seqvalcd 10336 hashfzo 10673 hashxp 10677 fsumconst 11328 modfsummod 11332 telfsumo 11340 fprodconst 11494 mulgcd 11871 algcvg 11896 phiprmpw 12065 strslfv3 12174 uptx 12613 resubmet 12887 |
Copyright terms: Public domain | W3C validator |