![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5eq | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5eq.1 |
![]() ![]() ![]() ![]() |
syl5eq.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl5eq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5eq.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | syl5eq.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtrd 2069 |
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: syl5req 2082 syl5eqr 2083 3eqtr3a 2093 3eqtr4g 2094 csbtt 2856 csbvarg 2871 csbie2g 2890 rabbi2dva 3139 csbprc 3256 disjssun 3279 disjpr2 3425 prprc2 3470 difprsn2 3495 opprc 3561 intsng 3640 riinm 3720 iinxsng 3721 rintm 3735 sucprc 4115 unisucg 4117 xpriindim 4417 relop 4429 dmxpm 4498 riinint 4536 resabs1 4583 resabs2 4584 resima2 4587 xpssres 4588 resopab2 4598 imasng 4633 ndmima 4645 xpdisj1 4690 xpdisj2 4691 djudisj 4693 resdisj 4694 rnxpm 4695 xpima1 4710 xpima2m 4711 dmsnsnsng 4741 rnsnopg 4742 rnpropg 4743 mptiniseg 4758 dfco2a 4764 relcoi1 4792 unixpm 4796 iotaval 4821 funtp 4895 fnun 4948 fnresdisj 4952 fnima 4960 fnimaeq0 4963 fcoi1 5013 f1orescnv 5085 foun 5088 resdif 5091 tz6.12-2 5112 fveu 5113 tz6.12-1 5143 fvun2 5183 fvopab3ig 5189 f1oresrab 5272 dfmptg 5285 ressnop0 5287 fvunsng 5300 fsnunfv 5306 fvpr1 5308 fvpr2 5309 fvpr1g 5310 fvpr2g 5311 fvtp1g 5312 fvtp2g 5313 fvtp3g 5314 fvtp2 5316 fvtp3 5317 f1oiso2 5409 riotaund 5445 ovprc 5482 resoprab2 5540 fnoprabg 5544 ovidig 5560 ovigg 5563 ov6g 5580 ovconst2 5594 offval2 5668 ot1stg 5721 ot2ndg 5722 ot3rdgg 5723 fmpt2co 5779 tpostpos2 5821 rdgisuc1 5911 frec0g 5922 frecsuclem1 5926 frecsuclem2 5928 frecrdg 5931 oasuc 5983 oa1suc 5986 omsuc 5990 nnm1 6033 nnm2 6034 dfec2 6045 errn 6064 1qec 6372 mulidnq 6373 addpinq1 6447 0idsr 6695 1idsr 6696 mulresr 6735 pitonnlem2 6743 ax1rid 6761 axcnre 6765 negid 7054 subneg 7056 negneg 7057 2times 7816 rexneg 8513 fseq1p1m1 8726 fzosplitprm1 8860 frec2uz0d 8866 frec2uzrdg 8876 frecuzrdg0 8881 iseqval 8900 sqval 8966 binom3 9019 reim0 9089 remullem 9099 |
Copyright terms: Public domain | W3C validator |