![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4g | Unicode version |
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3eqtr4g.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr4g.2 |
![]() ![]() ![]() ![]() |
3eqtr4g.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr4g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4g.2 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 3eqtr4g.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5eq 2081 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3eqtr4g.3 |
. 2
![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl6eqr 2087 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: rabeqf 2544 csbeq1 2849 csbeq2d 2868 csbnestgf 2892 difeq1 3049 difeq2 3050 uneq2 3085 ineq2 3126 dfrab3ss 3209 ifeq1 3328 ifeq2 3329 ifbi 3342 pweq 3354 sneq 3378 csbsng 3422 rabsn 3428 preq1 3438 preq2 3439 tpeq1 3447 tpeq2 3448 tpeq3 3449 prprc1 3469 opeq1 3540 opeq2 3541 oteq1 3549 oteq2 3550 oteq3 3551 csbunig 3579 unieq 3580 inteq 3609 iineq1 3662 iineq2 3665 dfiin2g 3681 iinrabm 3710 iinin1m 3717 iinxprg 3722 opabbid 3813 mpteq12f 3828 suceq 4105 xpeq1 4302 xpeq2 4303 csbxpg 4364 csbdmg 4472 rneq 4504 reseq1 4549 reseq2 4550 csbresg 4558 resmpt 4599 imaeq1 4606 imaeq2 4607 csbrng 4725 dmpropg 4736 rnpropg 4743 cores 4767 cores2 4776 xpcom 4807 iotaeq 4818 iotabi 4819 fntpg 4898 funimaexg 4926 fveq1 5120 fveq2 5121 fvres 5141 csbfv12g 5152 fnimapr 5176 fndmin 5217 fprg 5289 fsnunfv 5306 fsnunres 5307 fliftf 5382 isoini2 5401 riotaeqdv 5412 riotabidv 5413 riotauni 5417 riotabidva 5427 snriota 5440 oveq 5461 oveq1 5462 oveq2 5463 oprabbid 5500 mpt2eq123 5506 mpt2eq123dva 5508 mpt2eq3dva 5511 resmpt2 5541 ovres 5582 f1ocnvd 5644 ofeq 5656 ofreq 5657 ovtposg 5815 recseq 5862 tfr2a 5877 rdgeq1 5898 rdgeq2 5899 freceq1 5919 freceq2 5920 eceq1 6077 eceq2 6079 qseq1 6090 qseq2 6091 uniqs 6100 ecinxp 6117 qsinxp 6118 erovlem 6134 addpiord 6300 mulpiord 6301 00sr 6697 negeq 7001 csbnegg 7006 negsubdi 7063 mulneg1 7188 deceq1 8146 deceq2 8147 xnegeq 8510 fseq1p1m1 8726 frec2uzzd 8867 frec2uzsucd 8868 frec2uzrdg 8876 frecuzrdgsuc 8882 iseqeq1 8894 iseqeq2 8895 iseqeq3 8896 iseqeq4 8897 |
Copyright terms: Public domain | W3C validator |