![]() |
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 2044 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 3 | eqtri 2060 |
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 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: 3eqtr2i 2066 3eqtr2ri 2067 3eqtr4i 2070 3eqtr4ri 2071 rabab 2575 cbvralcsf 2908 cbvrexcsf 2909 cbvrabcsf 2911 dfin5 2925 dfdif2 2926 uneqin 3188 unrab 3208 inrab 3209 inrab2 3210 difrab 3211 dfrab3ss 3215 rabun2 3216 difidALT 3293 difdifdirss 3307 dfif3 3343 tpidm 3472 dfint2 3617 iunrab 3704 uniiun 3710 intiin 3711 0iin 3715 mptv 3853 xpundi 4396 xpundir 4397 resiun2 4631 resopab 4652 opabresid 4659 dfse2 4698 cnvun 4729 cnvin 4731 imaundir 4737 imainrect 4766 cnvcnv2 4774 cnvcnvres 4784 dmtpop 4796 rnsnopg 4799 rnco2 4828 dmco 4829 co01 4835 unidmrn 4850 dfdm2 4852 funimaexg 4983 dfmpt3 5021 mptun 5029 funcocnv2 5151 fnasrn 5341 fnasrng 5343 fpr 5345 fmptap 5353 riotav 5473 dmoprab 5585 rnoprab2 5588 mpt2v 5594 mpt2mptx 5595 abrexex2g 5747 abrexex2 5751 1stval2 5782 2ndval2 5783 fo1st 5784 fo2nd 5785 xp2 5799 dfoprab4f 5819 fmpt2co 5837 tposmpt2 5896 recsfval 5931 frecfnom 5986 frecsuclem1 5987 frecsuclem2 5989 df2o3 6014 o1p1e2 6048 ecqs 6168 qliftf 6191 erovlem 6198 dmaddpq 6477 dmmulpq 6478 enq0enq 6529 nqprlu 6645 m1p1sr 6845 m1m1sr 6846 caucvgsr 6886 dfcnqs 6917 3m1e2 8036 2p2e4 8037 3p2e5 8052 3p3e6 8053 4p2e6 8054 4p3e7 8055 4p4e8 8056 5p2e7 8057 5p3e8 8058 5p4e9 8059 5p5e10 8060 6p2e8 8061 6p3e9 8062 6p4e10 8063 7p2e9 8064 7p3e10 8065 8p2e10 8066 nn0supp 8234 nnzrab 8269 nn0zrab 8270 dec0u 8382 dec0h 8383 decsuc 8390 decsucc 8394 numma 8398 decma 8405 decmac 8406 decma2c 8407 decadd 8408 decaddc 8409 decmul1c 8414 decmul2c 8415 5t5e25 8443 6t6e36 8448 8t6e48 8459 nn0uz 8507 nnuz 8508 ioomax 8817 iccmax 8818 ioopos 8819 ioorp 8820 fseq1p1m1 8956 fzo0to2pr 9074 fzo0to3tp 9075 frecfzennn 9203 irec 9352 bj-omind 10058 |
Copyright terms: Public domain | W3C validator |