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 2153 | . 2 |
4 | 3eqtr2d.3 | . 2 | |
5 | 3, 4 | eqtrd 2150 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 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: fmptapd 5579 rdgisucinc 6250 ctm 6962 mulidnq 7165 ltrnqg 7196 recexprlem1ssl 7409 recexprlem1ssu 7410 ltmprr 7418 mulcmpblnrlemg 7516 caucvgsrlemoffcau 7574 negsub 7978 neg2sub 7990 divmuleqap 8445 divneg2ap 8464 qapne 9399 seqvalcd 10200 binom2 10371 bcpasc 10480 crim 10598 remullem 10611 max0addsup 10959 summodclem2a 11118 isum1p 11229 geo2sum 11251 cvgratz 11269 efi4p 11351 tanaddap 11373 addcos 11380 cos2tsin 11385 demoivreALT 11407 omeo 11522 sqgcd 11644 txrest 12372 limccnpcntop 12740 dvrecap 12773 cosq34lt1 12858 |
Copyright terms: Public domain | W3C validator |