![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr2d | Unicode version |
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3eqtr2d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr2d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr2d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr2d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3eqtr2d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtr4d 2225 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3eqtr2d.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtrd 2222 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: fmptapd 5728 rdgisucinc 6411 ctm 7139 mulidnq 7419 ltrnqg 7450 recexprlem1ssl 7663 recexprlem1ssu 7664 ltmprr 7672 mulcmpblnrlemg 7770 caucvgsrlemoffcau 7828 negsub 8236 neg2sub 8248 divmuleqap 8705 divneg2ap 8724 qapne 9671 seqvalcd 10492 binom2 10666 bcpasc 10781 crim 10902 remullem 10915 max0addsup 11263 summodclem2a 11424 isum1p 11535 geo2sum 11557 cvgratz 11575 efi4p 11760 tanaddap 11782 addcos 11789 cos2tsin 11794 demoivreALT 11816 omeo 11938 sqgcd 12065 eulerthlemth 12267 pythagtriplem16 12314 fldivp1 12383 pockthlem 12391 4sqlem10 12422 gsumval2 12875 grpinvid2 13012 imasgrp2 13067 mulgaddcomlem 13102 mulgmodid 13118 ablsubsub 13274 ablsubsub4 13275 opprunitd 13477 lmodfopne 13659 txrest 14253 limccnpcntop 14621 dvrecap 14654 cosq34lt1 14748 wilthlem1 14875 lgseisenlem1 14928 |
Copyright terms: Public domain | W3C validator |