![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtri | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.) |
Ref | Expression |
---|---|
3eqtri.1 |
![]() ![]() ![]() ![]() |
3eqtri.2 |
![]() ![]() ![]() ![]() |
3eqtri.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtri |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtri.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | 3eqtri.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 3eqtri.3 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtri 2057 |
. 2
![]() ![]() ![]() ![]() |
5 | 1, 4 | eqtri 2057 |
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: csbid 2853 un23 3096 in32 3143 dfrab2 3206 difun2 3296 tpidm23 3462 unisn 3587 dfiunv2 3684 uniop 3983 suc0 4114 unisuc 4116 iunsuc 4123 xpun 4344 dfrn2 4466 dfdmf 4471 dfrnf 4518 res0 4559 resres 4567 xpssres 4588 dfima2 4613 imai 4624 ima0 4627 imaundir 4680 xpima1 4710 xpima2m 4711 dmresv 4722 rescnvcnv 4726 dmtpop 4739 rnsnopg 4742 resdmres 4755 dmmpt 4759 dmco 4772 co01 4778 fpr 5288 fmptpr 5298 fvsnun2 5304 mpt20 5516 dmoprab 5527 rnoprab 5529 ov6g 5580 1st0 5713 2nd0 5714 dfmpt2 5786 algrflem 5792 dftpos2 5817 tposoprab 5836 tposmpt2 5837 tfrlem8 5875 df2o3 5953 axi2m1 6759 2p2e4 7815 numsuc 8155 numsucc 8169 xnegmnf 8512 fz0tp 8751 fzo0to2pr 8844 fzo0to3tp 8845 fzo0to42pr 8846 i4 9008 abs0 9222 absi 9223 |
Copyright terms: Public domain | W3C validator |