![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr4i | Unicode version |
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtr4i.1 |
![]() ![]() ![]() ![]() |
eqtr4i.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqtr4i |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | eqtr4i.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | eqcomi 2041 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 3 | 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: 3eqtr2i 2063 3eqtr2ri 2064 3eqtr4i 2067 3eqtr4ri 2068 rabab 2569 cbvralcsf 2902 cbvrexcsf 2903 cbvrabcsf 2905 dfin5 2919 dfdif2 2920 uneqin 3182 unrab 3202 inrab 3203 inrab2 3204 difrab 3205 dfrab3ss 3209 rabun2 3210 difidALT 3287 difdifdirss 3301 dfif3 3337 tpidm 3463 dfint2 3608 iunrab 3695 uniiun 3701 intiin 3702 0iin 3706 mptv 3844 xpundi 4339 xpundir 4340 resiun2 4574 resopab 4595 opabresid 4602 dfse2 4641 cnvun 4672 cnvin 4674 imaundir 4680 imainrect 4709 cnvcnv2 4717 cnvcnvres 4727 dmtpop 4739 rnsnopg 4742 rnco2 4771 dmco 4772 co01 4778 unidmrn 4793 dfdm2 4795 funimaexg 4926 dfmpt3 4964 mptun 4972 funcocnv2 5094 fnasrn 5284 fnasrng 5286 fpr 5288 fmptap 5296 riotav 5416 dmoprab 5527 rnoprab2 5530 mpt2v 5536 mpt2mptx 5537 abrexex2g 5689 abrexex2 5693 1stval2 5724 2ndval2 5725 fo1st 5726 fo2nd 5727 xp2 5741 dfoprab4f 5761 fmpt2co 5779 tposmpt2 5837 recsfval 5872 frecfnom 5925 frecsuclem1 5926 frecsuclem2 5928 df2o3 5953 o1p1e2 5987 ecqs 6104 qliftf 6127 erovlem 6134 dmaddpq 6363 dmmulpq 6364 enq0enq 6414 m1p1sr 6688 m1m1sr 6689 dfcnqs 6738 3m1e2 7814 2p2e4 7815 3p2e5 7830 3p3e6 7831 4p2e6 7832 4p3e7 7833 4p4e8 7834 5p2e7 7835 5p3e8 7836 5p4e9 7837 5p5e10 7838 6p2e8 7839 6p3e9 7840 6p4e10 7841 7p2e9 7842 7p3e10 7843 8p2e10 7844 nn0supp 8010 nnzrab 8045 nn0zrab 8046 dec0u 8158 dec0h 8159 decsuc 8166 decsucc 8170 numma 8174 decma 8181 decmac 8182 decma2c 8183 decadd 8184 decaddc 8185 decmul1c 8190 decmul2c 8191 5t5e25 8219 6t6e36 8224 8t6e48 8235 nn0uz 8283 nnuz 8284 ioomax 8587 iccmax 8588 ioopos 8589 ioorp 8590 fseq1p1m1 8726 fzo0to2pr 8844 fzo0to3tp 8845 frecfzennn 8884 irec 9005 bj-omind 9393 |
Copyright terms: Public domain | W3C validator |