![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4ri | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4i.1 |
![]() ![]() ![]() ![]() |
3eqtr4i.2 |
![]() ![]() ![]() ![]() |
3eqtr4i.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr4ri |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4i.3 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 3eqtr4i.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtr4i 2201 |
. 2
![]() ![]() ![]() ![]() |
4 | 3eqtr4i.2 |
. 2
![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtr4i 2201 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: cbvreucsf 3123 dfif6 3538 qdass 3691 tpidm12 3693 unipr 3825 dfdm4 4821 dmun 4836 resres 4921 inres 4926 resdifcom 4927 resiun1 4928 imainrect 5076 coundi 5132 coundir 5133 funopg 5252 offres 6139 mpomptsx 6201 cnvoprab 6238 snec 6599 halfpm6th 9142 numsucc 9426 decbin2 9527 fsumadd 11417 fsum2d 11446 fprodmul 11602 fprodfac 11626 fprodrec 11640 znnen 12402 |
Copyright terms: Public domain | W3C validator |