![]() |
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 2109 |
. 2
![]() ![]() ![]() ![]() |
5 | 1, 4 | eqtri 2109 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-4 1446 ax-17 1465 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 |
This theorem is referenced by: csbid 2941 un23 3160 in32 3213 dfrab2 3275 difun2 3366 tpidm23 3547 unisn 3675 dfiunv2 3772 uniop 4091 suc0 4247 unisuc 4249 iunsuc 4256 xpun 4512 dfrn2 4637 dfdmf 4642 dfrnf 4689 res0 4730 resres 4738 xpssres 4760 dfima2 4789 imai 4801 ima0 4804 imaundir 4858 xpima1 4890 xpima2m 4891 dmresv 4902 rescnvcnv 4906 dmtpop 4919 rnsnopg 4922 resdmres 4935 dmmpt 4939 dmco 4952 co01 4958 fpr 5493 fmptpr 5503 fvsnun2 5509 mpt20 5732 dmoprab 5743 rnoprab 5745 ov6g 5796 1st0 5929 2nd0 5930 dfmpt2 6002 algrflem 6008 dftpos2 6040 tposoprab 6059 tposmpt2 6060 tfrlem8 6097 frecsuc 6186 df2o3 6209 sbthlemi5 6724 sup00 6752 casedm 6831 djudm 6841 axi2m1 7471 2p2e4 8604 numsuc 8951 numsucc 8977 decmul10add 9006 5p5e10 9008 6p4e10 9009 7p3e10 9012 xnegmnf 9352 fz0tp 9596 fzo0to2pr 9690 fzo0to3tp 9691 fzo0to42pr 9692 0tonninf 9906 1tonninf 9907 inftonninf 9908 sq4e2t8 10113 i4 10118 fac1 10198 fac3 10201 abs0 10552 absi 10553 trirecip 10956 geoihalfsum 10977 esum 11013 tan0 11083 ef01bndlem 11108 3dvdsdec 11204 3dvds2dec 11205 3lcm2e6woprm 11407 6lcm4e12 11408 ndxarg 11578 setsfun 11590 setsfun0 11591 |
Copyright terms: Public domain | W3C validator |