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 2200 | . 2 |
4 | 3eqtr2d.3 | . 2 | |
5 | 3, 4 | eqtrd 2197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: fmptapd 5670 rdgisucinc 6344 ctm 7065 mulidnq 7321 ltrnqg 7352 recexprlem1ssl 7565 recexprlem1ssu 7566 ltmprr 7574 mulcmpblnrlemg 7672 caucvgsrlemoffcau 7730 negsub 8137 neg2sub 8149 divmuleqap 8604 divneg2ap 8623 qapne 9568 seqvalcd 10384 binom2 10555 bcpasc 10668 crim 10786 remullem 10799 max0addsup 11147 summodclem2a 11308 isum1p 11419 geo2sum 11441 cvgratz 11459 efi4p 11644 tanaddap 11666 addcos 11673 cos2tsin 11678 demoivreALT 11700 omeo 11820 sqgcd 11947 eulerthlemth 12141 pythagtriplem16 12188 fldivp1 12255 txrest 12817 limccnpcntop 13185 dvrecap 13218 cosq34lt1 13312 |
Copyright terms: Public domain | W3C validator |