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 2121 | . 2 |
4 | 1, 3 | eqtri 2138 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: 3eqtr2i 2144 3eqtr2ri 2145 3eqtr4i 2148 3eqtr4ri 2149 rabab 2681 cbvralcsf 3032 cbvrexcsf 3033 cbvrabcsf 3035 dfin5 3048 dfdif2 3049 uneqin 3297 unrab 3317 inrab 3318 inrab2 3319 difrab 3320 dfrab3ss 3324 rabun2 3325 difidALT 3402 difdifdirss 3417 dfif3 3457 tpidm 3595 dfint2 3743 iunrab 3830 uniiun 3836 intiin 3837 0iin 3841 mptv 3995 xpundi 4565 xpundir 4566 resiun2 4809 resopab 4833 opabresid 4842 dfse2 4882 cnvun 4914 cnvin 4916 imaundir 4922 imainrect 4954 cnvcnv2 4962 cnvcnvres 4972 dmtpop 4984 rnsnopg 4987 rnco2 5016 dmco 5017 co01 5023 unidmrn 5041 dfdm2 5043 funimaexg 5177 dfmpt3 5215 mptun 5224 funcocnv2 5360 fnasrn 5566 fnasrng 5568 fpr 5570 fmptap 5578 riotav 5703 dmoprab 5820 rnoprab2 5823 mpov 5829 mpomptx 5830 abrexex2g 5986 abrexex2 5990 1stval2 6021 2ndval2 6022 fo1st 6023 fo2nd 6024 xp2 6039 dfoprab4f 6059 fmpoco 6081 tposmpo 6146 recsfval 6180 frecfnom 6266 freccllem 6267 frecfcllem 6269 frecsuclem 6271 df2o3 6295 o1p1e2 6332 ecqs 6459 qliftf 6482 erovlem 6489 mapsnf1o3 6559 ixp0x 6588 xpf1o 6706 djuunr 6919 dmaddpq 7155 dmmulpq 7156 enq0enq 7207 nqprlu 7323 m1p1sr 7536 m1m1sr 7537 caucvgsr 7578 dfcnqs 7617 3m1e2 8808 2p2e4 8815 3p2e5 8829 3p3e6 8830 4p2e6 8831 4p3e7 8832 4p4e8 8833 5p2e7 8834 5p3e8 8835 5p4e9 8836 6p2e8 8837 6p3e9 8838 7p2e9 8839 nn0supp 8997 nnzrab 9046 nn0zrab 9047 dec0u 9170 dec0h 9171 decsuc 9180 decsucc 9190 numma 9193 decma 9200 decmac 9201 decma2c 9202 decadd 9203 decaddc 9204 decmul1 9213 decmul1c 9214 decmul2c 9215 5p5e10 9220 6p4e10 9221 7p3e10 9224 8p2e10 9229 5t5e25 9252 6t6e36 9257 8t6e48 9268 nn0uz 9328 nnuz 9329 xaddcom 9612 ioomax 9699 iccmax 9700 ioopos 9701 ioorp 9702 fseq1p1m1 9842 fzo0to2pr 9963 fzo0to3tp 9964 frecfzennn 10167 irec 10360 sq10e99m1 10428 facnn 10441 fac0 10442 faclbnd2 10456 zfz1isolemsplit 10549 minmax 10969 xrminmax 11002 fisumrev2 11183 fsumparts 11207 fsumiun 11214 isumnn0nn 11230 ege2le3 11304 cos1bnd 11393 efieq1re 11405 eirraplem 11410 phiprmpw 11825 unennn 11837 ennnfonelemjn 11842 qnnen 11871 strle1g 11976 tgrest 12265 uniretop 12621 dvexp 12771 dvef 12783 cospi 12808 sincos6thpi 12850 bj-omind 13059 |
Copyright terms: Public domain | W3C validator |