Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtr4rd | Unicode version |
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.) |
Ref | Expression |
---|---|
3eqtr4d.1 | |
3eqtr4d.2 | |
3eqtr4d.3 |
Ref | Expression |
---|---|
3eqtr4rd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4d.3 | . . 3 | |
2 | 3eqtr4d.1 | . . 3 | |
3 | 1, 2 | eqtr4d 2075 | . 2 |
4 | 3eqtr4d.2 | . 2 | |
5 | 3, 4 | eqtr4d 2075 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1243 |
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 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: csbcnvg 4519 phplem4 6318 phplem4on 6329 recexnq 6488 prarloclemcalc 6600 addcomprg 6676 mulcomprg 6678 mulcmpblnrlemg 6825 axmulass 6947 divnegap 7683 modqlt 9175 modqmulnn 9184 iseqcaopr3 9240 cjreb 9466 recj 9467 imcj 9475 imval2 9494 resqrexlemover 9608 sqrtmul 9633 amgm2 9714 |
Copyright terms: Public domain | W3C validator |